%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP144-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n025.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:34:22 EDT 2024
% Result : Satisfiable 0.85s 1.03s
% Output : Saturation 0.85s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c2,axiom,
( X202 != X201
| X198 != X197
| X196 != X195
| X200 != X199
| skf11(X202,X198,X196,X200) = skf11(X201,X197,X195,X199) ),
theory(equality) ).
cnf(c210,plain,
( X754 != X755
| X756 != X760
| X758 != X759
| skf11(X754,X756,X758,X757) = skf11(X755,X760,X759,X757) ),
inference(resolution,[status(thm)],[c2,reflexivity]) ).
cnf(c505,plain,
( X951 != X950
| X948 != X949
| skf11(X951,X948,X947,X946) = skf11(X950,X949,X947,X946) ),
inference(resolution,[status(thm)],[c210,reflexivity]) ).
cnf(c566,plain,
( X962 != X963
| skf11(X962,X959,X960,X961) = skf11(X963,X959,X960,X961) ),
inference(resolution,[status(thm)],[c505,reflexivity]) ).
cnf(c565,plain,
( X954 != X955
| skf11(X954,X954,X952,X953) = skf11(X955,X955,X952,X953) ),
inference(factor,[status(thm)],[c505]) ).
cnf(c504,plain,
( X931 != X930
| X932 != X929
| skf11(X931,X932,X932,X928) = skf11(X930,X929,X929,X928) ),
inference(factor,[status(thm)],[c210]) ).
cnf(c503,plain,
( X911 != X908
| X909 != X910
| skf11(X911,X909,X911,X907) = skf11(X908,X910,X908,X907) ),
inference(factor,[status(thm)],[c210]) ).
cnf(c558,plain,
( X924 != X926
| skf11(X924,X927,X924,X925) = skf11(X926,X927,X926,X925) ),
inference(resolution,[status(thm)],[c503,reflexivity]) ).
cnf(c557,plain,
( X921 != X920
| skf11(X921,X921,X921,X919) = skf11(X920,X920,X920,X919) ),
inference(factor,[status(thm)],[c503]) ).
cnf(c208,plain,
( X733 != X734
| X736 != X738
| X735 != X737
| skf11(X733,X736,X735,X736) = skf11(X734,X738,X737,X738) ),
inference(factor,[status(thm)],[c2]) ).
cnf(c493,plain,
( X870 != X868
| X871 != X869
| skf11(X870,X871,X867,X871) = skf11(X868,X869,X867,X869) ),
inference(resolution,[status(thm)],[c208,reflexivity]) ).
cnf(c492,plain,
( X863 != X866
| X864 != X865
| skf11(X863,X864,X864,X864) = skf11(X866,X865,X865,X865) ),
inference(factor,[status(thm)],[c208]) ).
cnf(c491,plain,
( X849 != X851
| X850 != X852
| skf11(X849,X850,X849,X850) = skf11(X851,X852,X851,X852) ),
inference(factor,[status(thm)],[c208]) ).
cnf(c207,plain,
( X723 != X726
| X721 != X725
| X722 != X724
| skf11(X723,X721,X722,X723) = skf11(X726,X725,X724,X726) ),
inference(factor,[status(thm)],[c2]) ).
cnf(c486,plain,
( X836 != X834
| X838 != X837
| skf11(X836,X838,X835,X836) = skf11(X834,X837,X835,X834) ),
inference(resolution,[status(thm)],[c207,reflexivity]) ).
cnf(c541,plain,
( X846 != X845
| skf11(X846,X848,X847,X846) = skf11(X845,X848,X847,X845) ),
inference(resolution,[status(thm)],[c486,reflexivity]) ).
cnf(c540,plain,
( X842 != X840
| skf11(X842,X842,X841,X842) = skf11(X840,X840,X841,X840) ),
inference(factor,[status(thm)],[c486]) ).
cnf(clause74,negated_conjecture,
two(skc7,skc8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause74) ).
cnf(clause60,axiom,
( ~ two(X126,X125)
| member(X126,skf10(X125,X126),X125) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause60) ).
cnf(c140,plain,
member(skc7,skf10(skc8,skc7),skc8),
inference(resolution,[status(thm)],[clause60,clause74]) ).
cnf(c5,axiom,
( X222 != X221
| X220 != X219
| X218 != X217
| ~ member(X222,X220,X218)
| member(X221,X219,X217) ),
theory(equality) ).
cnf(c217,plain,
( skc7 != X775
| skf10(skc8,skc7) != X777
| skc8 != X776
| member(X775,X777,X776) ),
inference(resolution,[status(thm)],[c5,c140]) ).
cnf(c514,plain,
( skc7 != X833
| skc8 != X832
| member(X833,skf10(skc8,skc7),X832) ),
inference(resolution,[status(thm)],[c217,reflexivity]) ).
cnf(c539,plain,
( skc7 != X839
| member(X839,skf10(skc8,skc7),skc8) ),
inference(resolution,[status(thm)],[c514,reflexivity]) ).
cnf(c485,plain,
( X820 != X821
| X819 != X822
| skf11(X820,X819,X819,X820) = skf11(X821,X822,X822,X821) ),
inference(factor,[status(thm)],[c207]) ).
cnf(c484,plain,
( X808 != X811
| X810 != X809
| skf11(X808,X810,X808,X808) = skf11(X811,X809,X811,X811) ),
inference(factor,[status(thm)],[c207]) ).
cnf(c532,plain,
( X817 != X818
| skf11(X817,X816,X817,X817) = skf11(X818,X816,X818,X818) ),
inference(resolution,[status(thm)],[c484,reflexivity]) ).
cnf(c531,plain,
( X813 != X814
| skf11(X813,X813,X813,X813) = skf11(X814,X814,X814,X814) ),
inference(factor,[status(thm)],[c484]) ).
cnf(clause61,axiom,
( ~ two(X132,X131)
| member(X132,skf8(X131,X132),X131) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause61) ).
cnf(c142,plain,
member(skc7,skf8(skc8,skc7),skc8),
inference(resolution,[status(thm)],[clause61,clause74]) ).
cnf(c216,plain,
( skc7 != X767
| skf8(skc8,skc7) != X769
| skc8 != X768
| member(X767,X769,X768) ),
inference(resolution,[status(thm)],[c5,c142]) ).
cnf(c510,plain,
( skc7 != X807
| skc8 != X806
| member(X807,skf8(skc8,skc7),X806) ),
inference(resolution,[status(thm)],[c216,reflexivity]) ).
cnf(c530,plain,
( skc7 != X812
| member(X812,skf8(skc8,skc7),skc8) ),
inference(resolution,[status(thm)],[c510,reflexivity]) ).
cnf(clause86,negated_conjecture,
agent(skc7,skc12,skc16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause86) ).
cnf(c63,axiom,
( X660 != X659
| X658 != X657
| X656 != X655
| ~ agent(X660,X658,X656)
| agent(X659,X657,X655) ),
theory(equality) ).
cnf(c446,plain,
( skc7 != X801
| skc12 != X800
| skc16 != X802
| agent(X801,X800,X802) ),
inference(resolution,[status(thm)],[c63,clause86]) ).
cnf(c527,plain,
( skc7 != X803
| skc12 != X804
| agent(X803,X804,skc16) ),
inference(resolution,[status(thm)],[c446,reflexivity]) ).
cnf(c528,plain,
( skc7 != X805
| agent(X805,skc12,skc16) ),
inference(resolution,[status(thm)],[c527,reflexivity]) ).
cnf(clause85,negated_conjecture,
down(skc7,skc12,skc13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause85) ).
cnf(c62,axiom,
( X648 != X647
| X646 != X645
| X644 != X643
| ~ down(X648,X646,X644)
| down(X647,X645,X643) ),
theory(equality) ).
cnf(c441,plain,
( skc7 != X793
| skc12 != X792
| skc13 != X791
| down(X793,X792,X791) ),
inference(resolution,[status(thm)],[c62,clause85]) ).
cnf(c522,plain,
( skc7 != X797
| skc12 != X798
| down(X797,X798,skc13) ),
inference(resolution,[status(thm)],[c441,reflexivity]) ).
cnf(c525,plain,
( skc7 != X799
| down(X799,skc12,skc13) ),
inference(resolution,[status(thm)],[c522,reflexivity]) ).
cnf(clause84,negated_conjecture,
in(skc7,skc12,skc15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause84) ).
cnf(c61,axiom,
( X636 != X635
| X634 != X633
| X632 != X631
| ~ in(X636,X634,X632)
| in(X635,X633,X631) ),
theory(equality) ).
cnf(c439,plain,
( skc7 != X789
| skc12 != X790
| skc15 != X788
| in(X789,X790,X788) ),
inference(resolution,[status(thm)],[c61,clause84]) ).
cnf(c521,plain,
( skc7 != X795
| skc12 != X794
| in(X795,X794,skc15) ),
inference(resolution,[status(thm)],[c439,reflexivity]) ).
cnf(c523,plain,
( skc7 != X796
| in(X796,skc12,skc15) ),
inference(resolution,[status(thm)],[c521,reflexivity]) ).
cnf(clause83,negated_conjecture,
of(skc7,skc14,skc15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause83) ).
cnf(c55,axiom,
( X621 != X620
| X619 != X618
| X617 != X616
| ~ of(X621,X619,X617)
| of(X620,X618,X616) ),
theory(equality) ).
cnf(c434,plain,
( skc7 != X784
| skc14 != X783
| skc15 != X782
| of(X784,X783,X782) ),
inference(resolution,[status(thm)],[c55,clause83]) ).
cnf(c518,plain,
( skc7 != X786
| skc14 != X785
| of(X786,X785,skc15) ),
inference(resolution,[status(thm)],[c434,reflexivity]) ).
cnf(c519,plain,
( skc7 != X787
| of(X787,skc14,skc15) ),
inference(resolution,[status(thm)],[c518,reflexivity]) ).
cnf(clause87,negated_conjecture,
( ~ member(skc7,X133,skc8)
| young(skc7,X133) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause87) ).
cnf(c147,plain,
young(skc7,skf10(skc8,skc7)),
inference(resolution,[status(thm)],[c140,clause87]) ).
cnf(c53,axiom,
( X589 != X588
| X586 != X587
| ~ young(X589,X586)
| young(X588,X587) ),
theory(equality) ).
cnf(c426,plain,
( skc7 != X780
| skf10(skc8,skc7) != X779
| young(X780,X779) ),
inference(resolution,[status(thm)],[c53,c147]) ).
cnf(c516,plain,
( skc7 != X781
| young(X781,skf10(skc8,skc7)) ),
inference(resolution,[status(thm)],[c426,reflexivity]) ).
cnf(c174,plain,
young(skc7,skf8(skc8,skc7)),
inference(resolution,[status(thm)],[c142,clause87]) ).
cnf(c425,plain,
( skc7 != X774
| skf8(skc8,skc7) != X773
| young(X774,X773) ),
inference(resolution,[status(thm)],[c53,c174]) ).
cnf(c513,plain,
( skc7 != X778
| young(X778,skf8(skc8,skc7)) ),
inference(resolution,[status(thm)],[c425,reflexivity]) ).
cnf(clause14,axiom,
( ~ man(X30,X29)
| male(X30,X29) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause14) ).
cnf(clause2,axiom,
( ~ fellow(X6,X5)
| man(X6,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
cnf(clause88,negated_conjecture,
( ~ member(skc7,X136,skc8)
| fellow(skc7,X136) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause88) ).
cnf(c148,plain,
fellow(skc7,skf10(skc8,skc7)),
inference(resolution,[status(thm)],[c140,clause88]) ).
cnf(c151,plain,
man(skc7,skf10(skc8,skc7)),
inference(resolution,[status(thm)],[c148,clause2]) ).
cnf(c153,plain,
male(skc7,skf10(skc8,skc7)),
inference(resolution,[status(thm)],[c151,clause14]) ).
cnf(c19,axiom,
( X312 != X311
| X309 != X310
| ~ male(X312,X309)
| male(X311,X310) ),
theory(equality) ).
cnf(c292,plain,
( skc7 != X770
| skf10(skc8,skc7) != X771
| male(X770,X771) ),
inference(resolution,[status(thm)],[c19,c153]) ).
cnf(c511,plain,
( skc7 != X772
| male(X772,skf10(skc8,skc7)) ),
inference(resolution,[status(thm)],[c292,reflexivity]) ).
cnf(c175,plain,
fellow(skc7,skf8(skc8,skc7)),
inference(resolution,[status(thm)],[c142,clause88]) ).
cnf(c179,plain,
man(skc7,skf8(skc8,skc7)),
inference(resolution,[status(thm)],[c175,clause2]) ).
cnf(c181,plain,
male(skc7,skf8(skc8,skc7)),
inference(resolution,[status(thm)],[c179,clause14]) ).
cnf(c291,plain,
( skc7 != X764
| skf8(skc8,skc7) != X765
| male(X764,X765) ),
inference(resolution,[status(thm)],[c19,c181]) ).
cnf(c508,plain,
( skc7 != X766
| male(X766,skf8(skc8,skc7)) ),
inference(resolution,[status(thm)],[c291,reflexivity]) ).
cnf(clause13,axiom,
( ~ human_person(X28,X27)
| animate(X28,X27) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause13) ).
cnf(clause3,axiom,
( ~ man(X8,X7)
| human_person(X8,X7) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause3) ).
cnf(c152,plain,
human_person(skc7,skf10(skc8,skc7)),
inference(resolution,[status(thm)],[c151,clause3]) ).
cnf(c154,plain,
animate(skc7,skf10(skc8,skc7)),
inference(resolution,[status(thm)],[c152,clause13]) ).
cnf(c18,axiom,
( X304 != X303
| X301 != X302
| ~ animate(X304,X301)
| animate(X303,X302) ),
theory(equality) ).
cnf(c287,plain,
( skc7 != X761
| skf10(skc8,skc7) != X762
| animate(X761,X762) ),
inference(resolution,[status(thm)],[c18,c154]) ).
cnf(c506,plain,
( skc7 != X763
| animate(X763,skf10(skc8,skc7)) ),
inference(resolution,[status(thm)],[c287,reflexivity]) ).
cnf(c180,plain,
human_person(skc7,skf8(skc8,skc7)),
inference(resolution,[status(thm)],[c179,clause3]) ).
cnf(c182,plain,
animate(skc7,skf8(skc8,skc7)),
inference(resolution,[status(thm)],[c180,clause13]) ).
cnf(c286,plain,
( skc7 != X751
| skf8(skc8,skc7) != X752
| animate(X751,X752) ),
inference(resolution,[status(thm)],[c18,c182]) ).
cnf(c501,plain,
( skc7 != X753
| animate(X753,skf8(skc8,skc7)) ),
inference(resolution,[status(thm)],[c286,reflexivity]) ).
cnf(clause12,axiom,
( ~ human_person(X26,X25)
| human(X26,X25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause12) ).
cnf(c183,plain,
human(skc7,skf8(skc8,skc7)),
inference(resolution,[status(thm)],[c180,clause12]) ).
cnf(c17,axiom,
( X295 != X294
| X292 != X293
| ~ human(X295,X292)
| human(X294,X293) ),
theory(equality) ).
cnf(c282,plain,
( skc7 != X743
| skf8(skc8,skc7) != X742
| human(X743,X742) ),
inference(resolution,[status(thm)],[c17,c183]) ).
cnf(c496,plain,
( skc7 != X750
| human(X750,skf8(skc8,skc7)) ),
inference(resolution,[status(thm)],[c282,reflexivity]) ).
cnf(c209,plain,
( X744 != X745
| X746 != X748
| X747 != X749
| skf11(X744,X746,X747,X747) = skf11(X745,X748,X749,X749) ),
inference(factor,[status(thm)],[c2]) ).
cnf(c155,plain,
human(skc7,skf10(skc8,skc7)),
inference(resolution,[status(thm)],[c152,clause12]) ).
cnf(c281,plain,
( skc7 != X740
| skf10(skc8,skc7) != X739
| human(X740,X739) ),
inference(resolution,[status(thm)],[c17,c155]) ).
cnf(c494,plain,
( skc7 != X741
| human(X741,skf10(skc8,skc7)) ),
inference(resolution,[status(thm)],[c281,reflexivity]) ).
cnf(clause11,axiom,
( ~ organism(X24,X23)
| living(X24,X23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause11) ).
cnf(clause4,axiom,
( ~ human_person(X10,X9)
| organism(X10,X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
cnf(c156,plain,
organism(skc7,skf10(skc8,skc7)),
inference(resolution,[status(thm)],[c152,clause4]) ).
cnf(c159,plain,
living(skc7,skf10(skc8,skc7)),
inference(resolution,[status(thm)],[c156,clause11]) ).
cnf(c16,axiom,
( X285 != X284
| X282 != X283
| ~ living(X285,X282)
| living(X284,X283) ),
theory(equality) ).
cnf(c276,plain,
( skc7 != X730
| skf10(skc8,skc7) != X731
| living(X730,X731) ),
inference(resolution,[status(thm)],[c16,c159]) ).
cnf(c489,plain,
( skc7 != X732
| living(X732,skf10(skc8,skc7)) ),
inference(resolution,[status(thm)],[c276,reflexivity]) ).
cnf(c184,plain,
organism(skc7,skf8(skc8,skc7)),
inference(resolution,[status(thm)],[c180,clause4]) ).
cnf(c189,plain,
living(skc7,skf8(skc8,skc7)),
inference(resolution,[status(thm)],[c184,clause11]) ).
cnf(c275,plain,
( skc7 != X727
| skf8(skc8,skc7) != X728
| living(X727,X728) ),
inference(resolution,[status(thm)],[c16,c189]) ).
cnf(c487,plain,
( skc7 != X729
| living(X729,skf8(skc8,skc7)) ),
inference(resolution,[status(thm)],[c275,reflexivity]) ).
cnf(clause10,axiom,
( ~ organism(X22,X21)
| impartial(X22,X21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause10) ).
cnf(c188,plain,
impartial(skc7,skf8(skc8,skc7)),
inference(resolution,[status(thm)],[c184,clause10]) ).
cnf(c15,axiom,
( X277 != X276
| X274 != X275
| ~ impartial(X277,X274)
| impartial(X276,X275) ),
theory(equality) ).
cnf(c269,plain,
( skc7 != X718
| skf8(skc8,skc7) != X719
| impartial(X718,X719) ),
inference(resolution,[status(thm)],[c15,c188]) ).
cnf(c482,plain,
( skc7 != X720
| impartial(X720,skf8(skc8,skc7)) ),
inference(resolution,[status(thm)],[c269,reflexivity]) ).
cnf(c158,plain,
impartial(skc7,skf10(skc8,skc7)),
inference(resolution,[status(thm)],[c156,clause10]) ).
cnf(c268,plain,
( skc7 != X715
| skf10(skc8,skc7) != X716
| impartial(X715,X716) ),
inference(resolution,[status(thm)],[c15,c158]) ).
cnf(c480,plain,
( skc7 != X717
| impartial(X717,skf10(skc8,skc7)) ),
inference(resolution,[status(thm)],[c268,reflexivity]) ).
cnf(clause91,negated_conjecture,
( ~ member(skc7,X176,skc8)
| ~ frontseat(skc7,X176)
| be(skc7,skf6(X176),X176,skf5(X176)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause91) ).
cnf(c192,plain,
( ~ frontseat(skc7,skf10(skc8,skc7))
| be(skc7,skf6(skf10(skc8,skc7)),skf10(skc8,skc7),skf5(skf10(skc8,skc7))) ),
inference(resolution,[status(thm)],[clause91,c140]) ).
cnf(clause9,axiom,
( ~ entity(X20,X19)
| existent(X20,X19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause9) ).
cnf(clause5,axiom,
( ~ organism(X12,X11)
| entity(X12,X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause5) ).
cnf(c190,plain,
entity(skc7,skf8(skc8,skc7)),
inference(resolution,[status(thm)],[c184,clause5]) ).
cnf(c194,plain,
existent(skc7,skf8(skc8,skc7)),
inference(resolution,[status(thm)],[c190,clause9]) ).
cnf(c14,axiom,
( X268 != X267
| X265 != X266
| ~ existent(X268,X265)
| existent(X267,X266) ),
theory(equality) ).
cnf(c260,plain,
( skc7 != X712
| skf8(skc8,skc7) != X713
| existent(X712,X713) ),
inference(resolution,[status(thm)],[c14,c194]) ).
cnf(c478,plain,
( skc7 != X714
| existent(X714,skf8(skc8,skc7)) ),
inference(resolution,[status(thm)],[c260,reflexivity]) ).
cnf(c191,plain,
( ~ frontseat(skc7,skf8(skc8,skc7))
| be(skc7,skf6(skf8(skc8,skc7)),skf8(skc8,skc7),skf5(skf8(skc8,skc7))) ),
inference(resolution,[status(thm)],[clause91,c142]) ).
cnf(c160,plain,
entity(skc7,skf10(skc8,skc7)),
inference(resolution,[status(thm)],[c156,clause5]) ).
cnf(c164,plain,
existent(skc7,skf10(skc8,skc7)),
inference(resolution,[status(thm)],[c160,clause9]) ).
cnf(c259,plain,
( skc7 != X709
| skf10(skc8,skc7) != X710
| existent(X709,X710) ),
inference(resolution,[status(thm)],[c14,c164]) ).
cnf(c476,plain,
( skc7 != X711
| existent(X711,skf10(skc8,skc7)) ),
inference(resolution,[status(thm)],[c259,reflexivity]) ).
cnf(clause8,axiom,
( ~ entity(X18,X17)
| specific(X18,X17) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
cnf(c165,plain,
specific(skc7,skf10(skc8,skc7)),
inference(resolution,[status(thm)],[c160,clause8]) ).
cnf(c13,axiom,
( X258 != X257
| X255 != X256
| ~ specific(X258,X255)
| specific(X257,X256) ),
theory(equality) ).
cnf(c254,plain,
( skc7 != X706
| skf10(skc8,skc7) != X707
| specific(X706,X707) ),
inference(resolution,[status(thm)],[c13,c165]) ).
cnf(c474,plain,
( skc7 != X708
| specific(X708,skf10(skc8,skc7)) ),
inference(resolution,[status(thm)],[c254,reflexivity]) ).
cnf(clause90,negated_conjecture,
( ~ member(skc7,X175,skc8)
| ~ frontseat(skc7,X175)
| in(skc7,skf5(X175),X175) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause90) ).
cnf(c186,plain,
( ~ frontseat(skc7,skf10(skc8,skc7))
| in(skc7,skf5(skf10(skc8,skc7)),skf10(skc8,skc7)) ),
inference(resolution,[status(thm)],[clause90,c140]) ).
cnf(c195,plain,
specific(skc7,skf8(skc8,skc7)),
inference(resolution,[status(thm)],[c190,clause8]) ).
cnf(c251,plain,
( skc7 != X703
| skf8(skc8,skc7) != X704
| specific(X703,X704) ),
inference(resolution,[status(thm)],[c13,c195]) ).
cnf(c472,plain,
( skc7 != X705
| specific(X705,skf8(skc8,skc7)) ),
inference(resolution,[status(thm)],[c251,reflexivity]) ).
cnf(clause7,axiom,
( ~ thing(X16,X15)
| singleton(X16,X15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause7) ).
cnf(clause6,axiom,
( ~ entity(X14,X13)
| thing(X14,X13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause6) ).
cnf(c193,plain,
thing(skc7,skf8(skc8,skc7)),
inference(resolution,[status(thm)],[c190,clause6]) ).
cnf(c196,plain,
singleton(skc7,skf8(skc8,skc7)),
inference(resolution,[status(thm)],[c193,clause7]) ).
cnf(c12,axiom,
( X250 != X249
| X247 != X248
| ~ singleton(X250,X247)
| singleton(X249,X248) ),
theory(equality) ).
cnf(c245,plain,
( skc7 != X700
| skf8(skc8,skc7) != X701
| singleton(X700,X701) ),
inference(resolution,[status(thm)],[c12,c196]) ).
cnf(c470,plain,
( skc7 != X702
| singleton(X702,skf8(skc8,skc7)) ),
inference(resolution,[status(thm)],[c245,reflexivity]) ).
cnf(c185,plain,
( ~ frontseat(skc7,skf8(skc8,skc7))
| in(skc7,skf5(skf8(skc8,skc7)),skf8(skc8,skc7)) ),
inference(resolution,[status(thm)],[clause90,c142]) ).
cnf(c163,plain,
thing(skc7,skf10(skc8,skc7)),
inference(resolution,[status(thm)],[c160,clause6]) ).
cnf(c166,plain,
singleton(skc7,skf10(skc8,skc7)),
inference(resolution,[status(thm)],[c163,clause7]) ).
cnf(c244,plain,
( skc7 != X697
| skf10(skc8,skc7) != X698
| singleton(X697,X698) ),
inference(resolution,[status(thm)],[c12,c166]) ).
cnf(c468,plain,
( skc7 != X699
| singleton(X699,skf10(skc8,skc7)) ),
inference(resolution,[status(thm)],[c244,reflexivity]) ).
cnf(c11,axiom,
( X241 != X240
| X238 != X239
| ~ thing(X241,X238)
| thing(X240,X239) ),
theory(equality) ).
cnf(c235,plain,
( skc7 != X694
| skf8(skc8,skc7) != X695
| thing(X694,X695) ),
inference(resolution,[status(thm)],[c11,c193]) ).
cnf(c466,plain,
( skc7 != X696
| thing(X696,skf8(skc8,skc7)) ),
inference(resolution,[status(thm)],[c235,reflexivity]) ).
cnf(c232,plain,
( skc7 != X691
| skf10(skc8,skc7) != X692
| thing(X691,X692) ),
inference(resolution,[status(thm)],[c11,c163]) ).
cnf(c464,plain,
( skc7 != X693
| thing(X693,skf10(skc8,skc7)) ),
inference(resolution,[status(thm)],[c232,reflexivity]) ).
cnf(c10,axiom,
( X234 != X233
| X231 != X232
| ~ entity(X234,X231)
| entity(X233,X232) ),
theory(equality) ).
cnf(c223,plain,
( skc7 != X687
| skf10(skc8,skc7) != X688
| entity(X687,X688) ),
inference(resolution,[status(thm)],[c10,c160]) ).
cnf(c462,plain,
( skc7 != X689
| entity(X689,skf10(skc8,skc7)) ),
inference(resolution,[status(thm)],[c223,reflexivity]) ).
cnf(c222,plain,
( skc7 != X683
| skf8(skc8,skc7) != X684
| entity(X683,X684) ),
inference(resolution,[status(thm)],[c10,c190]) ).
cnf(c459,plain,
( skc7 != X686
| entity(X686,skf8(skc8,skc7)) ),
inference(resolution,[status(thm)],[c222,reflexivity]) ).
cnf(clause67,axiom,
( ~ placename(X172,X170)
| ~ of(X172,X169,X171)
| ~ placename(X172,X169)
| ~ of(X172,X170,X171)
| ~ entity(X172,X171)
| X169 = X170 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause67) ).
cnf(c170,plain,
( ~ placename(skc7,skc14)
| ~ of(skc7,X685,skc15)
| ~ placename(skc7,X685)
| ~ entity(skc7,skc15)
| X685 = skc14 ),
inference(resolution,[status(thm)],[clause67,clause83]) ).
cnf(c9,axiom,
( X230 != X229
| X227 != X228
| ~ organism(X230,X227)
| organism(X229,X228) ),
theory(equality) ).
cnf(c221,plain,
( skc7 != X680
| skf8(skc8,skc7) != X681
| organism(X680,X681) ),
inference(resolution,[status(thm)],[c9,c184]) ).
cnf(c457,plain,
( skc7 != X682
| organism(X682,skf8(skc8,skc7)) ),
inference(resolution,[status(thm)],[c221,reflexivity]) ).
cnf(c220,plain,
( skc7 != X676
| skf10(skc8,skc7) != X677
| organism(X676,X677) ),
inference(resolution,[status(thm)],[c9,c156]) ).
cnf(c455,plain,
( skc7 != X678
| organism(X678,skf10(skc8,skc7)) ),
inference(resolution,[status(thm)],[c220,reflexivity]) ).
cnf(c8,axiom,
( X226 != X225
| X223 != X224
| ~ human_person(X226,X223)
| human_person(X225,X224) ),
theory(equality) ).
cnf(c219,plain,
( skc7 != X674
| skf10(skc8,skc7) != X673
| human_person(X674,X673) ),
inference(resolution,[status(thm)],[c8,c152]) ).
cnf(c453,plain,
( skc7 != X675
| human_person(X675,skf10(skc8,skc7)) ),
inference(resolution,[status(thm)],[c219,reflexivity]) ).
cnf(c218,plain,
( skc7 != X668
| skf8(skc8,skc7) != X667
| human_person(X668,X667) ),
inference(resolution,[status(thm)],[c8,c180]) ).
cnf(c451,plain,
( skc7 != X669
| human_person(X669,skf8(skc8,skc7)) ),
inference(resolution,[status(thm)],[c218,reflexivity]) ).
cnf(c7,axiom,
( X216 != X215
| X213 != X214
| ~ man(X216,X213)
| man(X215,X214) ),
theory(equality) ).
cnf(c215,plain,
( skc7 != X665
| skf8(skc8,skc7) != X664
| man(X665,X664) ),
inference(resolution,[status(thm)],[c7,c179]) ).
cnf(c449,plain,
( skc7 != X666
| man(X666,skf8(skc8,skc7)) ),
inference(resolution,[status(thm)],[c215,reflexivity]) ).
cnf(c214,plain,
( skc7 != X662
| skf10(skc8,skc7) != X661
| man(X662,X661) ),
inference(resolution,[status(thm)],[c7,c151]) ).
cnf(c447,plain,
( skc7 != X663
| man(X663,skf10(skc8,skc7)) ),
inference(resolution,[status(thm)],[c214,reflexivity]) ).
cnf(c6,axiom,
( X212 != X211
| X209 != X210
| ~ fellow(X212,X209)
| fellow(X211,X210) ),
theory(equality) ).
cnf(c213,plain,
( skc7 != X653
| skf10(skc8,skc7) != X652
| fellow(X653,X652) ),
inference(resolution,[status(thm)],[c6,c148]) ).
cnf(c444,plain,
( skc7 != X654
| fellow(X654,skf10(skc8,skc7)) ),
inference(resolution,[status(thm)],[c213,reflexivity]) ).
cnf(c212,plain,
( skc7 != X650
| skf8(skc8,skc7) != X649
| fellow(X650,X649) ),
inference(resolution,[status(thm)],[c6,c175]) ).
cnf(c442,plain,
( skc7 != X651
| fellow(X651,skf8(skc8,skc7)) ),
inference(resolution,[status(thm)],[c212,reflexivity]) ).
cnf(clause89,negated_conjecture,
( ~ member(skc7,X174,skc8)
| ~ frontseat(skc7,X174)
| state(skc7,skf6(X173)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause89) ).
cnf(c177,plain,
( ~ frontseat(skc7,skf10(skc8,skc7))
| state(skc7,skf6(X642)) ),
inference(resolution,[status(thm)],[clause89,c140]) ).
cnf(c176,plain,
( ~ frontseat(skc7,skf8(skc8,skc7))
| state(skc7,skf6(X641)) ),
inference(resolution,[status(thm)],[clause89,c142]) ).
cnf(clause81,negated_conjecture,
dirty(skc7,skc16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause81) ).
cnf(c60,axiom,
( X628 != X627
| X625 != X626
| ~ dirty(X628,X625)
| dirty(X627,X626) ),
theory(equality) ).
cnf(c437,plain,
( skc7 != X630
| skc16 != X629
| dirty(X630,X629) ),
inference(resolution,[status(thm)],[c60,clause81]) ).
cnf(c438,plain,
( skc7 != X637
| dirty(X637,skc16) ),
inference(resolution,[status(thm)],[c437,reflexivity]) ).
cnf(clause80,negated_conjecture,
white(skc7,skc16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause80) ).
cnf(c59,axiom,
( X615 != X614
| X612 != X613
| ~ white(X615,X612)
| white(X614,X613) ),
theory(equality) ).
cnf(c433,plain,
( skc7 != X622
| skc16 != X623
| white(X622,X623) ),
inference(resolution,[status(thm)],[c59,clause80]) ).
cnf(c435,plain,
( skc7 != X624
| white(X624,skc16) ),
inference(resolution,[status(thm)],[c433,reflexivity]) ).
cnf(clause78,negated_conjecture,
present(skc7,skc12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause78) ).
cnf(c58,axiom,
( X608 != X607
| X605 != X606
| ~ present(X608,X605)
| present(X607,X606) ),
theory(equality) ).
cnf(c430,plain,
( skc7 != X610
| skc12 != X609
| present(X610,X609) ),
inference(resolution,[status(thm)],[c58,clause78]) ).
cnf(c431,plain,
( skc7 != X611
| present(X611,skc12) ),
inference(resolution,[status(thm)],[c430,reflexivity]) ).
cnf(c54,axiom,
( X604 != X603
| X600 != X599
| X598 != X597
| X602 != X601
| ~ be(X604,X600,X598,X602)
| be(X603,X599,X597,X601) ),
theory(equality) ).
cnf(clause71,negated_conjecture,
lonely(skc7,skc13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause71) ).
cnf(c57,axiom,
( X593 != X592
| X590 != X591
| ~ lonely(X593,X590)
| lonely(X592,X591) ),
theory(equality) ).
cnf(c427,plain,
( skc7 != X594
| skc13 != X595
| lonely(X594,X595) ),
inference(resolution,[status(thm)],[c57,clause71]) ).
cnf(c428,plain,
( skc7 != X596
| lonely(X596,skc13) ),
inference(resolution,[status(thm)],[c427,reflexivity]) ).
cnf(clause82,negated_conjecture,
old(skc7,skc16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause82) ).
cnf(c52,axiom,
( X582 != X581
| X579 != X580
| ~ old(X582,X579)
| old(X581,X580) ),
theory(equality) ).
cnf(c422,plain,
( skc7 != X584
| skc16 != X583
| old(X584,X583) ),
inference(resolution,[status(thm)],[c52,clause82]) ).
cnf(c423,plain,
( skc7 != X585
| old(X585,skc16) ),
inference(resolution,[status(thm)],[c422,reflexivity]) ).
cnf(c51,axiom,
( X578 != X577
| X575 != X576
| ~ furniture(X578,X575)
| furniture(X577,X576) ),
theory(equality) ).
cnf(c50,axiom,
( X574 != X573
| X571 != X572
| ~ seat(X574,X571)
| seat(X573,X572) ),
theory(equality) ).
cnf(c49,axiom,
( X570 != X569
| X567 != X568
| ~ frontseat(X570,X567)
| frontseat(X569,X568) ),
theory(equality) ).
cnf(clause70,negated_conjecture,
city(skc7,skc15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause70) ).
cnf(clause46,axiom,
( ~ city(X94,X93)
| location(X94,X93) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause46) ).
cnf(c108,plain,
location(skc7,skc15),
inference(resolution,[status(thm)],[clause46,clause70]) ).
cnf(c48,axiom,
( X562 != X561
| X559 != X560
| ~ location(X562,X559)
| location(X561,X560) ),
theory(equality) ).
cnf(c418,plain,
( skc7 != X565
| skc15 != X564
| location(X565,X564) ),
inference(resolution,[status(thm)],[c48,c108]) ).
cnf(c420,plain,
( skc7 != X566
| location(X566,skc15) ),
inference(resolution,[status(thm)],[c418,reflexivity]) ).
cnf(c47,axiom,
( X556 != X555
| X553 != X554
| ~ city(X556,X553)
| city(X555,X554) ),
theory(equality) ).
cnf(c416,plain,
( skc7 != X557
| skc15 != X558
| city(X557,X558) ),
inference(resolution,[status(thm)],[c47,clause70]) ).
cnf(c417,plain,
( skc7 != X563
| city(X563,skc15) ),
inference(resolution,[status(thm)],[c416,reflexivity]) ).
cnf(clause76,negated_conjecture,
hollywood_placename(skc7,skc14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause76) ).
cnf(c46,axiom,
( X549 != X548
| X546 != X547
| ~ hollywood_placename(X549,X546)
| hollywood_placename(X548,X547) ),
theory(equality) ).
cnf(c413,plain,
( skc7 != X551
| skc14 != X550
| hollywood_placename(X551,X550) ),
inference(resolution,[status(thm)],[c46,clause76]) ).
cnf(c414,plain,
( skc7 != X552
| hollywood_placename(X552,skc14) ),
inference(resolution,[status(thm)],[c413,reflexivity]) ).
cnf(clause75,negated_conjecture,
placename(skc7,skc14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause75) ).
cnf(clause38,axiom,
( ~ placename(X78,X77)
| relname(X78,X77) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
cnf(c98,plain,
relname(skc7,skc14),
inference(resolution,[status(thm)],[clause38,clause75]) ).
cnf(clause39,axiom,
( ~ relname(X80,X79)
| relation(X80,X79) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause39) ).
cnf(c100,plain,
relation(skc7,skc14),
inference(resolution,[status(thm)],[clause39,c98]) ).
cnf(clause40,axiom,
( ~ relation(X82,X81)
| abstraction(X82,X81) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause40) ).
cnf(c101,plain,
abstraction(skc7,skc14),
inference(resolution,[status(thm)],[clause40,c100]) ).
cnf(clause43,axiom,
( ~ abstraction(X88,X87)
| general(X88,X87) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause43) ).
cnf(c105,plain,
general(skc7,skc14),
inference(resolution,[status(thm)],[clause43,c101]) ).
cnf(c45,axiom,
( X541 != X540
| X538 != X539
| ~ general(X541,X538)
| general(X540,X539) ),
theory(equality) ).
cnf(c409,plain,
( skc7 != X543
| skc14 != X544
| general(X543,X544) ),
inference(resolution,[status(thm)],[c45,c105]) ).
cnf(c411,plain,
( skc7 != X545
| general(X545,skc14) ),
inference(resolution,[status(thm)],[c409,reflexivity]) ).
cnf(clause42,axiom,
( ~ abstraction(X86,X85)
| nonhuman(X86,X85) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause42) ).
cnf(c103,plain,
nonhuman(skc7,skc14),
inference(resolution,[status(thm)],[clause42,c101]) ).
cnf(c44,axiom,
( X535 != X534
| X532 != X533
| ~ nonhuman(X535,X532)
| nonhuman(X534,X533) ),
theory(equality) ).
cnf(c407,plain,
( skc7 != X536
| skc14 != X537
| nonhuman(X536,X537) ),
inference(resolution,[status(thm)],[c44,c103]) ).
cnf(c408,plain,
( skc7 != X542
| nonhuman(X542,skc14) ),
inference(resolution,[status(thm)],[c407,reflexivity]) ).
cnf(c43,axiom,
( X528 != X527
| X525 != X526
| ~ abstraction(X528,X525)
| abstraction(X527,X526) ),
theory(equality) ).
cnf(c404,plain,
( skc7 != X529
| skc14 != X530
| abstraction(X529,X530) ),
inference(resolution,[status(thm)],[c43,c101]) ).
cnf(c405,plain,
( skc7 != X531
| abstraction(X531,skc14) ),
inference(resolution,[status(thm)],[c404,reflexivity]) ).
cnf(c42,axiom,
( X520 != X519
| X517 != X518
| ~ relation(X520,X517)
| relation(X519,X518) ),
theory(equality) ).
cnf(c400,plain,
( skc7 != X523
| skc14 != X522
| relation(X523,X522) ),
inference(resolution,[status(thm)],[c42,c100]) ).
cnf(c402,plain,
( skc7 != X524
| relation(X524,skc14) ),
inference(resolution,[status(thm)],[c400,reflexivity]) ).
cnf(c41,axiom,
( X511 != X510
| X508 != X509
| ~ relname(X511,X508)
| relname(X510,X509) ),
theory(equality) ).
cnf(c396,plain,
( skc7 != X516
| skc14 != X515
| relname(X516,X515) ),
inference(resolution,[status(thm)],[c41,c98]) ).
cnf(c399,plain,
( skc7 != X521
| relname(X521,skc14) ),
inference(resolution,[status(thm)],[c396,reflexivity]) ).
cnf(c40,axiom,
( X501 != X500
| X498 != X499
| ~ placename(X501,X498)
| placename(X500,X499) ),
theory(equality) ).
cnf(c391,plain,
( skc7 != X513
| skc14 != X512
| placename(X513,X512) ),
inference(resolution,[status(thm)],[c40,clause75]) ).
cnf(c397,plain,
( skc7 != X514
| placename(X514,skc14) ),
inference(resolution,[status(thm)],[c391,reflexivity]) ).
cnf(clause72,negated_conjecture,
street(skc7,skc13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause72) ).
cnf(clause36,axiom,
( ~ street(X74,X73)
| way(X74,X73) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause36) ).
cnf(c88,plain,
way(skc7,skc13),
inference(resolution,[status(thm)],[clause36,clause72]) ).
cnf(c39,axiom,
( X493 != X492
| X490 != X491
| ~ way(X493,X490)
| way(X492,X491) ),
theory(equality) ).
cnf(c387,plain,
( skc7 != X505
| skc13 != X506
| way(X505,X506) ),
inference(resolution,[status(thm)],[c39,c88]) ).
cnf(c394,plain,
( skc7 != X507
| way(X507,skc13) ),
inference(resolution,[status(thm)],[c387,reflexivity]) ).
cnf(c38,axiom,
( X484 != X483
| X481 != X482
| ~ street(X484,X481)
| street(X483,X482) ),
theory(equality) ).
cnf(c383,plain,
( skc7 != X503
| skc13 != X502
| street(X503,X502) ),
inference(resolution,[status(thm)],[c38,clause72]) ).
cnf(c392,plain,
( skc7 != X504
| street(X504,skc13) ),
inference(resolution,[status(thm)],[c383,reflexivity]) ).
cnf(clause33,axiom,
( ~ object(X68,X67)
| nonliving(X68,X67) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause33) ).
cnf(clause31,axiom,
( ~ artifact(X64,X63)
| object(X64,X63) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause31) ).
cnf(clause37,axiom,
( ~ way(X76,X75)
| artifact(X76,X75) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
cnf(c89,plain,
artifact(skc7,skc13),
inference(resolution,[status(thm)],[clause37,c88]) ).
cnf(c90,plain,
object(skc7,skc13),
inference(resolution,[status(thm)],[c89,clause31]) ).
cnf(c94,plain,
nonliving(skc7,skc13),
inference(resolution,[status(thm)],[c90,clause33]) ).
cnf(c37,axiom,
( X474 != X473
| X471 != X472
| ~ nonliving(X474,X471)
| nonliving(X473,X472) ),
theory(equality) ).
cnf(c378,plain,
( skc7 != X496
| skc13 != X495
| nonliving(X496,X495) ),
inference(resolution,[status(thm)],[c37,c94]) ).
cnf(c389,plain,
( skc7 != X497
| nonliving(X497,skc13) ),
inference(resolution,[status(thm)],[c378,reflexivity]) ).
cnf(clause47,axiom,
( ~ location(X96,X95)
| object(X96,X95) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause47) ).
cnf(c109,plain,
object(skc7,skc15),
inference(resolution,[status(thm)],[clause47,c108]) ).
cnf(c113,plain,
nonliving(skc7,skc15),
inference(resolution,[status(thm)],[c109,clause33]) ).
cnf(c377,plain,
( skc7 != X489
| skc15 != X488
| nonliving(X489,X488) ),
inference(resolution,[status(thm)],[c37,c113]) ).
cnf(c386,plain,
( skc7 != X494
| nonliving(X494,skc15) ),
inference(resolution,[status(thm)],[c377,reflexivity]) ).
cnf(clause69,negated_conjecture,
chevy(skc7,skc16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause69) ).
cnf(clause26,axiom,
( ~ chevy(X54,X53)
| car(X54,X53) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause26) ).
cnf(c74,plain,
car(skc7,skc16),
inference(resolution,[status(thm)],[clause26,clause69]) ).
cnf(clause27,axiom,
( ~ car(X56,X55)
| vehicle(X56,X55) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause27) ).
cnf(c75,plain,
vehicle(skc7,skc16),
inference(resolution,[status(thm)],[clause27,c74]) ).
cnf(clause28,axiom,
( ~ vehicle(X58,X57)
| transport(X58,X57) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause28) ).
cnf(c76,plain,
transport(skc7,skc16),
inference(resolution,[status(thm)],[clause28,c75]) ).
cnf(clause29,axiom,
( ~ transport(X60,X59)
| instrumentality(X60,X59) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause29) ).
cnf(c77,plain,
instrumentality(skc7,skc16),
inference(resolution,[status(thm)],[clause29,c76]) ).
cnf(clause30,axiom,
( ~ instrumentality(X62,X61)
| artifact(X62,X61) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause30) ).
cnf(c78,plain,
artifact(skc7,skc16),
inference(resolution,[status(thm)],[clause30,c77]) ).
cnf(c79,plain,
object(skc7,skc16),
inference(resolution,[status(thm)],[clause31,c78]) ).
cnf(c84,plain,
nonliving(skc7,skc16),
inference(resolution,[status(thm)],[clause33,c79]) ).
cnf(c376,plain,
( skc7 != X486
| skc16 != X485
| nonliving(X486,X485) ),
inference(resolution,[status(thm)],[c37,c84]) ).
cnf(c384,plain,
( skc7 != X487
| nonliving(X487,skc16) ),
inference(resolution,[status(thm)],[c376,reflexivity]) ).
cnf(c36,axiom,
( X466 != X465
| X463 != X464
| ~ object(X466,X463)
| object(X465,X464) ),
theory(equality) ).
cnf(c372,plain,
( skc7 != X479
| skc13 != X478
| object(X479,X478) ),
inference(resolution,[status(thm)],[c36,c90]) ).
cnf(c381,plain,
( skc7 != X480
| object(X480,skc13) ),
inference(resolution,[status(thm)],[c372,reflexivity]) ).
cnf(c371,plain,
( skc7 != X476
| skc15 != X475
| object(X476,X475) ),
inference(resolution,[status(thm)],[c36,c109]) ).
cnf(c379,plain,
( skc7 != X477
| object(X477,skc15) ),
inference(resolution,[status(thm)],[c371,reflexivity]) ).
cnf(c370,plain,
( skc7 != X469
| skc16 != X468
| object(X469,X468) ),
inference(resolution,[status(thm)],[c36,c79]) ).
cnf(c374,plain,
( skc7 != X470
| object(X470,skc16) ),
inference(resolution,[status(thm)],[c370,reflexivity]) ).
cnf(c35,axiom,
( X457 != X456
| X454 != X455
| ~ artifact(X457,X454)
| artifact(X456,X455) ),
theory(equality) ).
cnf(c366,plain,
( skc7 != X462
| skc13 != X461
| artifact(X462,X461) ),
inference(resolution,[status(thm)],[c35,c89]) ).
cnf(c369,plain,
( skc7 != X467
| artifact(X467,skc13) ),
inference(resolution,[status(thm)],[c366,reflexivity]) ).
cnf(c365,plain,
( skc7 != X459
| skc16 != X458
| artifact(X459,X458) ),
inference(resolution,[status(thm)],[c35,c78]) ).
cnf(c367,plain,
( skc7 != X460
| artifact(X460,skc16) ),
inference(resolution,[status(thm)],[c365,reflexivity]) ).
cnf(c34,axiom,
( X447 != X446
| X444 != X445
| ~ instrumentality(X447,X444)
| instrumentality(X446,X445) ),
theory(equality) ).
cnf(c360,plain,
( skc7 != X451
| skc16 != X452
| instrumentality(X451,X452) ),
inference(resolution,[status(thm)],[c34,c77]) ).
cnf(c363,plain,
( skc7 != X453
| instrumentality(X453,skc16) ),
inference(resolution,[status(thm)],[c360,reflexivity]) ).
cnf(c33,axiom,
( X439 != X438
| X436 != X437
| ~ transport(X439,X436)
| transport(X438,X437) ),
theory(equality) ).
cnf(c356,plain,
( skc7 != X449
| skc16 != X448
| transport(X449,X448) ),
inference(resolution,[status(thm)],[c33,c76]) ).
cnf(c361,plain,
( skc7 != X450
| transport(X450,skc16) ),
inference(resolution,[status(thm)],[c356,reflexivity]) ).
cnf(c32,axiom,
( X430 != X429
| X427 != X428
| ~ vehicle(X430,X427)
| vehicle(X429,X428) ),
theory(equality) ).
cnf(c352,plain,
( skc7 != X442
| skc16 != X441
| vehicle(X442,X441) ),
inference(resolution,[status(thm)],[c32,c75]) ).
cnf(c358,plain,
( skc7 != X443
| vehicle(X443,skc16) ),
inference(resolution,[status(thm)],[c352,reflexivity]) ).
cnf(c31,axiom,
( X420 != X419
| X417 != X418
| ~ car(X420,X417)
| car(X419,X418) ),
theory(equality) ).
cnf(c347,plain,
( skc7 != X435
| skc16 != X434
| car(X435,X434) ),
inference(resolution,[status(thm)],[c31,c74]) ).
cnf(c355,plain,
( skc7 != X440
| car(X440,skc16) ),
inference(resolution,[status(thm)],[c347,reflexivity]) ).
cnf(c30,axiom,
( X412 != X411
| X409 != X410
| ~ chevy(X412,X409)
| chevy(X411,X410) ),
theory(equality) ).
cnf(c343,plain,
( skc7 != X432
| skc16 != X431
| chevy(X432,X431) ),
inference(resolution,[status(thm)],[c30,clause69]) ).
cnf(c353,plain,
( skc7 != X433
| chevy(X433,skc16) ),
inference(resolution,[status(thm)],[c343,reflexivity]) ).
cnf(clause79,negated_conjecture,
barrel(skc7,skc12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause79) ).
cnf(c29,axiom,
( X403 != X402
| X400 != X401
| ~ barrel(X403,X400)
| barrel(X402,X401) ),
theory(equality) ).
cnf(c339,plain,
( skc7 != X425
| skc12 != X424
| barrel(X425,X424) ),
inference(resolution,[status(thm)],[c29,clause79]) ).
cnf(c350,plain,
( skc7 != X426
| barrel(X426,skc12) ),
inference(resolution,[status(thm)],[c339,reflexivity]) ).
cnf(clause77,negated_conjecture,
event(skc7,skc12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause77) ).
cnf(c28,axiom,
( X393 != X392
| X390 != X391
| ~ event(X393,X390)
| event(X392,X391) ),
theory(equality) ).
cnf(c334,plain,
( skc7 != X422
| skc12 != X421
| event(X422,X421) ),
inference(resolution,[status(thm)],[c28,clause77]) ).
cnf(c348,plain,
( skc7 != X423
| event(X423,skc12) ),
inference(resolution,[status(thm)],[c334,reflexivity]) ).
cnf(clause44,axiom,
( ~ abstraction(X90,X89)
| unisex(X90,X89) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause44) ).
cnf(c106,plain,
unisex(skc7,skc14),
inference(resolution,[status(thm)],[clause44,c101]) ).
cnf(c27,axiom,
( X385 != X384
| X382 != X383
| ~ unisex(X385,X382)
| unisex(X384,X383) ),
theory(equality) ).
cnf(c330,plain,
( skc7 != X415
| skc14 != X414
| unisex(X415,X414) ),
inference(resolution,[status(thm)],[c27,c106]) ).
cnf(c345,plain,
( skc7 != X416
| unisex(X416,skc14) ),
inference(resolution,[status(thm)],[c330,reflexivity]) ).
cnf(clause35,axiom,
( ~ object(X72,X71)
| unisex(X72,X71) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause35) ).
cnf(c111,plain,
unisex(skc7,skc15),
inference(resolution,[status(thm)],[c109,clause35]) ).
cnf(c329,plain,
( skc7 != X408
| skc15 != X407
| unisex(X408,X407) ),
inference(resolution,[status(thm)],[c27,c111]) ).
cnf(c342,plain,
( skc7 != X413
| unisex(X413,skc15) ),
inference(resolution,[status(thm)],[c329,reflexivity]) ).
cnf(clause22,axiom,
( ~ eventuality(X46,X45)
| unisex(X46,X45) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause22) ).
cnf(clause24,axiom,
( ~ event(X50,X49)
| eventuality(X50,X49) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause24) ).
cnf(c67,plain,
eventuality(skc7,skc12),
inference(resolution,[status(thm)],[clause24,clause77]) ).
cnf(c68,plain,
unisex(skc7,skc12),
inference(resolution,[status(thm)],[c67,clause22]) ).
cnf(c328,plain,
( skc7 != X405
| skc12 != X404
| unisex(X405,X404) ),
inference(resolution,[status(thm)],[c27,c68]) ).
cnf(c340,plain,
( skc7 != X406
| unisex(X406,skc12) ),
inference(resolution,[status(thm)],[c328,reflexivity]) ).
cnf(c92,plain,
unisex(skc7,skc13),
inference(resolution,[status(thm)],[c90,clause35]) ).
cnf(c327,plain,
( skc7 != X398
| skc13 != X397
| unisex(X398,X397) ),
inference(resolution,[status(thm)],[c27,c92]) ).
cnf(c337,plain,
( skc7 != X399
| unisex(X399,skc13) ),
inference(resolution,[status(thm)],[c327,reflexivity]) ).
cnf(c87,plain,
unisex(skc7,skc16),
inference(resolution,[status(thm)],[clause35,c79]) ).
cnf(c326,plain,
( skc7 != X395
| skc16 != X394
| unisex(X395,X394) ),
inference(resolution,[status(thm)],[c27,c87]) ).
cnf(c335,plain,
( skc7 != X396
| unisex(X396,skc16) ),
inference(resolution,[status(thm)],[c326,reflexivity]) ).
cnf(clause21,axiom,
( ~ eventuality(X44,X43)
| nonexistent(X44,X43) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause21) ).
cnf(c70,plain,
nonexistent(skc7,skc12),
inference(resolution,[status(thm)],[c67,clause21]) ).
cnf(c26,axiom,
( X376 != X375
| X373 != X374
| ~ nonexistent(X376,X373)
| nonexistent(X375,X374) ),
theory(equality) ).
cnf(c322,plain,
( skc7 != X387
| skc12 != X388
| nonexistent(X387,X388) ),
inference(resolution,[status(thm)],[c26,c70]) ).
cnf(c332,plain,
( skc7 != X389
| nonexistent(X389,skc12) ),
inference(resolution,[status(thm)],[c322,reflexivity]) ).
cnf(c25,axiom,
( X366 != X365
| X363 != X364
| ~ eventuality(X366,X363)
| eventuality(X365,X364) ),
theory(equality) ).
cnf(c317,plain,
( skc7 != X381
| skc12 != X380
| eventuality(X381,X380) ),
inference(resolution,[status(thm)],[c25,c67]) ).
cnf(c325,plain,
( skc7 != X386
| eventuality(X386,skc12) ),
inference(resolution,[status(thm)],[c317,reflexivity]) ).
cnf(c23,axiom,
( X349 != X348
| X346 != X347
| ~ two(X349,X346)
| two(X348,X347) ),
theory(equality) ).
cnf(c310,plain,
( skc7 != X377
| skc8 != X378
| two(X377,X378) ),
inference(resolution,[status(thm)],[c23,clause74]) ).
cnf(c323,plain,
( skc7 != X379
| two(X379,skc8) ),
inference(resolution,[status(thm)],[c310,reflexivity]) ).
cnf(clause73,negated_conjecture,
group(skc7,skc8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause73) ).
cnf(clause15,axiom,
( ~ group(X32,X31)
| set(X32,X31) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause15) ).
cnf(c64,plain,
set(skc7,skc8),
inference(resolution,[status(thm)],[clause15,clause73]) ).
cnf(clause16,axiom,
( ~ set(X34,X33)
| multiple(X34,X33) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause16) ).
cnf(c65,plain,
multiple(skc7,skc8),
inference(resolution,[status(thm)],[clause16,c64]) ).
cnf(c22,axiom,
( X339 != X338
| X336 != X337
| ~ multiple(X339,X336)
| multiple(X338,X337) ),
theory(equality) ).
cnf(c305,plain,
( skc7 != X370
| skc8 != X371
| multiple(X370,X371) ),
inference(resolution,[status(thm)],[c22,c65]) ).
cnf(c320,plain,
( skc7 != X372
| multiple(X372,skc8) ),
inference(resolution,[status(thm)],[c305,reflexivity]) ).
cnf(c21,axiom,
( X331 != X330
| X328 != X329
| ~ set(X331,X328)
| set(X330,X329) ),
theory(equality) ).
cnf(c301,plain,
( skc7 != X367
| skc8 != X368
| set(X367,X368) ),
inference(resolution,[status(thm)],[c21,c64]) ).
cnf(c318,plain,
( skc7 != X369
| set(X369,skc8) ),
inference(resolution,[status(thm)],[c301,reflexivity]) ).
cnf(c20,axiom,
( X322 != X321
| X319 != X320
| ~ group(X322,X319)
| group(X321,X320) ),
theory(equality) ).
cnf(c297,plain,
( skc7 != X361
| skc8 != X360
| group(X361,X360) ),
inference(resolution,[status(thm)],[c20,clause73]) ).
cnf(c315,plain,
( skc7 != X362
| group(X362,skc8) ),
inference(resolution,[status(thm)],[c297,reflexivity]) ).
cnf(clause34,axiom,
( ~ object(X70,X69)
| impartial(X70,X69) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause34) ).
cnf(c93,plain,
impartial(skc7,skc13),
inference(resolution,[status(thm)],[c90,clause34]) ).
cnf(c271,plain,
( skc7 != X353
| skc13 != X354
| impartial(X353,X354) ),
inference(resolution,[status(thm)],[c15,c93]) ).
cnf(c313,plain,
( skc7 != X359
| impartial(X359,skc13) ),
inference(resolution,[status(thm)],[c271,reflexivity]) ).
cnf(c24,axiom,
( X358 != X357
| X355 != X356
| ~ state(X358,X355)
| state(X357,X356) ),
theory(equality) ).
cnf(c112,plain,
impartial(skc7,skc15),
inference(resolution,[status(thm)],[c109,clause34]) ).
cnf(c270,plain,
( skc7 != X350
| skc15 != X351
| impartial(X350,X351) ),
inference(resolution,[status(thm)],[c15,c112]) ).
cnf(c311,plain,
( skc7 != X352
| impartial(X352,skc15) ),
inference(resolution,[status(thm)],[c270,reflexivity]) ).
cnf(c86,plain,
impartial(skc7,skc16),
inference(resolution,[status(thm)],[clause34,c79]) ).
cnf(c267,plain,
( skc7 != X343
| skc16 != X344
| impartial(X343,X344) ),
inference(resolution,[status(thm)],[c15,c86]) ).
cnf(c308,plain,
( skc7 != X345
| impartial(X345,skc16) ),
inference(resolution,[status(thm)],[c267,reflexivity]) ).
cnf(clause32,axiom,
( ~ object(X66,X65)
| entity(X66,X65) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause32) ).
cnf(c91,plain,
entity(skc7,skc13),
inference(resolution,[status(thm)],[c90,clause32]) ).
cnf(c96,plain,
existent(skc7,skc13),
inference(resolution,[status(thm)],[c91,clause9]) ).
cnf(c263,plain,
( skc7 != X340
| skc13 != X341
| existent(X340,X341) ),
inference(resolution,[status(thm)],[c14,c96]) ).
cnf(c306,plain,
( skc7 != X342
| existent(X342,skc13) ),
inference(resolution,[status(thm)],[c263,reflexivity]) ).
cnf(c110,plain,
entity(skc7,skc15),
inference(resolution,[status(thm)],[c109,clause32]) ).
cnf(c115,plain,
existent(skc7,skc15),
inference(resolution,[status(thm)],[c110,clause9]) ).
cnf(c262,plain,
( skc7 != X333
| skc15 != X334
| existent(X333,X334) ),
inference(resolution,[status(thm)],[c14,c115]) ).
cnf(c303,plain,
( skc7 != X335
| existent(X335,skc15) ),
inference(resolution,[status(thm)],[c262,reflexivity]) ).
cnf(c80,plain,
entity(skc7,skc16),
inference(resolution,[status(thm)],[clause32,c79]) ).
cnf(c82,plain,
existent(skc7,skc16),
inference(resolution,[status(thm)],[c80,clause9]) ).
cnf(c261,plain,
( skc7 != X326
| skc16 != X327
| existent(X326,X327) ),
inference(resolution,[status(thm)],[c14,c82]) ).
cnf(c300,plain,
( skc7 != X332
| existent(X332,skc16) ),
inference(resolution,[status(thm)],[c261,reflexivity]) ).
cnf(clause20,axiom,
( ~ eventuality(X42,X41)
| specific(X42,X41) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause20) ).
cnf(c69,plain,
specific(skc7,skc12),
inference(resolution,[status(thm)],[c67,clause20]) ).
cnf(c253,plain,
( skc7 != X323
| skc12 != X324
| specific(X323,X324) ),
inference(resolution,[status(thm)],[c13,c69]) ).
cnf(c298,plain,
( skc7 != X325
| specific(X325,skc12) ),
inference(resolution,[status(thm)],[c253,reflexivity]) ).
cnf(c97,plain,
specific(skc7,skc13),
inference(resolution,[status(thm)],[c91,clause8]) ).
cnf(c252,plain,
( skc7 != X316
| skc13 != X317
| specific(X316,X317) ),
inference(resolution,[status(thm)],[c13,c97]) ).
cnf(c295,plain,
( skc7 != X318
| specific(X318,skc13) ),
inference(resolution,[status(thm)],[c252,reflexivity]) ).
cnf(c83,plain,
specific(skc7,skc16),
inference(resolution,[status(thm)],[c80,clause8]) ).
cnf(c250,plain,
( skc7 != X313
| skc16 != X314
| specific(X313,X314) ),
inference(resolution,[status(thm)],[c13,c83]) ).
cnf(c293,plain,
( skc7 != X315
| specific(X315,skc16) ),
inference(resolution,[status(thm)],[c250,reflexivity]) ).
cnf(c116,plain,
specific(skc7,skc15),
inference(resolution,[status(thm)],[c110,clause8]) ).
cnf(c249,plain,
( skc7 != X306
| skc15 != X307
| specific(X306,X307) ),
inference(resolution,[status(thm)],[c13,c116]) ).
cnf(c289,plain,
( skc7 != X308
| specific(X308,skc15) ),
inference(resolution,[status(thm)],[c249,reflexivity]) ).
cnf(clause19,axiom,
( ~ eventuality(X40,X39)
| thing(X40,X39) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause19) ).
cnf(c71,plain,
thing(skc7,skc12),
inference(resolution,[status(thm)],[c67,clause19]) ).
cnf(c73,plain,
singleton(skc7,skc12),
inference(resolution,[status(thm)],[c71,clause7]) ).
cnf(c243,plain,
( skc7 != X299
| skc12 != X300
| singleton(X299,X300) ),
inference(resolution,[status(thm)],[c12,c73]) ).
cnf(c285,plain,
( skc7 != X305
| singleton(X305,skc12) ),
inference(resolution,[status(thm)],[c243,reflexivity]) ).
cnf(c114,plain,
thing(skc7,skc15),
inference(resolution,[status(thm)],[c110,clause6]) ).
cnf(c117,plain,
singleton(skc7,skc15),
inference(resolution,[status(thm)],[c114,clause7]) ).
cnf(c242,plain,
( skc7 != X296
| skc15 != X297
| singleton(X296,X297) ),
inference(resolution,[status(thm)],[c12,c117]) ).
cnf(c283,plain,
( skc7 != X298
| singleton(X298,skc15) ),
inference(resolution,[status(thm)],[c242,reflexivity]) ).
cnf(clause41,axiom,
( ~ abstraction(X84,X83)
| thing(X84,X83) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause41) ).
cnf(c102,plain,
thing(skc7,skc14),
inference(resolution,[status(thm)],[clause41,c101]) ).
cnf(c104,plain,
singleton(skc7,skc14),
inference(resolution,[status(thm)],[c102,clause7]) ).
cnf(c241,plain,
( skc7 != X289
| skc14 != X290
| singleton(X289,X290) ),
inference(resolution,[status(thm)],[c12,c104]) ).
cnf(c279,plain,
( skc7 != X291
| singleton(X291,skc14) ),
inference(resolution,[status(thm)],[c241,reflexivity]) ).
cnf(c81,plain,
thing(skc7,skc16),
inference(resolution,[status(thm)],[c80,clause6]) ).
cnf(c85,plain,
singleton(skc7,skc16),
inference(resolution,[status(thm)],[c81,clause7]) ).
cnf(c240,plain,
( skc7 != X286
| skc16 != X287
| singleton(X286,X287) ),
inference(resolution,[status(thm)],[c12,c85]) ).
cnf(c277,plain,
( skc7 != X288
| singleton(X288,skc16) ),
inference(resolution,[status(thm)],[c240,reflexivity]) ).
cnf(c95,plain,
thing(skc7,skc13),
inference(resolution,[status(thm)],[c91,clause6]) ).
cnf(c99,plain,
singleton(skc7,skc13),
inference(resolution,[status(thm)],[c95,clause7]) ).
cnf(c239,plain,
( skc7 != X279
| skc13 != X280
| singleton(X279,X280) ),
inference(resolution,[status(thm)],[c12,c99]) ).
cnf(c273,plain,
( skc7 != X281
| singleton(X281,skc13) ),
inference(resolution,[status(thm)],[c239,reflexivity]) ).
cnf(c234,plain,
( skc7 != X272
| skc16 != X273
| thing(X272,X273) ),
inference(resolution,[status(thm)],[c11,c81]) ).
cnf(c266,plain,
( skc7 != X278
| thing(X278,skc16) ),
inference(resolution,[status(thm)],[c234,reflexivity]) ).
cnf(c233,plain,
( skc7 != X269
| skc15 != X270
| thing(X269,X270) ),
inference(resolution,[status(thm)],[c11,c114]) ).
cnf(c264,plain,
( skc7 != X271
| thing(X271,skc15) ),
inference(resolution,[status(thm)],[c233,reflexivity]) ).
cnf(c231,plain,
( skc7 != X262
| skc14 != X263
| thing(X262,X263) ),
inference(resolution,[status(thm)],[c11,c102]) ).
cnf(c257,plain,
( skc7 != X264
| thing(X264,skc14) ),
inference(resolution,[status(thm)],[c231,reflexivity]) ).
cnf(c230,plain,
( skc7 != X259
| skc12 != X260
| thing(X259,X260) ),
inference(resolution,[status(thm)],[c11,c71]) ).
cnf(c255,plain,
( skc7 != X261
| thing(X261,skc12) ),
inference(resolution,[status(thm)],[c230,reflexivity]) ).
cnf(c229,plain,
( skc7 != X252
| skc13 != X253
| thing(X252,X253) ),
inference(resolution,[status(thm)],[c11,c95]) ).
cnf(c247,plain,
( skc7 != X254
| thing(X254,skc13) ),
inference(resolution,[status(thm)],[c229,reflexivity]) ).
cnf(c226,plain,
( skc7 != X245
| skc13 != X246
| entity(X245,X246) ),
inference(resolution,[status(thm)],[c10,c91]) ).
cnf(c238,plain,
( skc7 != X251
| entity(X251,skc13) ),
inference(resolution,[status(thm)],[c226,reflexivity]) ).
cnf(c225,plain,
( skc7 != X242
| skc16 != X243
| entity(X242,X243) ),
inference(resolution,[status(thm)],[c10,c80]) ).
cnf(c236,plain,
( skc7 != X244
| entity(X244,skc16) ),
inference(resolution,[status(thm)],[c225,reflexivity]) ).
cnf(c224,plain,
( skc7 != X235
| skc15 != X236
| entity(X235,X236) ),
inference(resolution,[status(thm)],[c10,c110]) ).
cnf(c227,plain,
( skc7 != X237
| entity(X237,skc15) ),
inference(resolution,[status(thm)],[c224,reflexivity]) ).
cnf(c1,axiom,
( X184 != X183
| X181 != X182
| skf8(X184,X181) = skf8(X183,X182) ),
theory(equality) ).
cnf(c203,plain,
( X205 != X204
| skf8(X205,X206) = skf8(X204,X206) ),
inference(resolution,[status(thm)],[c1,reflexivity]) ).
cnf(c202,plain,
( X193 != X194
| skf8(X193,X193) = skf8(X194,X194) ),
inference(factor,[status(thm)],[c1]) ).
cnf(c0,axiom,
( X180 != X179
| X177 != X178
| skf10(X180,X177) = skf10(X179,X178) ),
theory(equality) ).
cnf(c199,plain,
( X188 != X189
| skf10(X188,X190) = skf10(X189,X190) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(c198,plain,
( X186 != X185
| skf10(X186,X186) = skf10(X185,X185) ),
inference(factor,[status(thm)],[c0]) ).
cnf(clause54,axiom,
( ~ multiple(X110,X109)
| ~ singleton(X110,X109) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause54) ).
cnf(c201,plain,
~ multiple(skc7,skf8(skc8,skc7)),
inference(resolution,[status(thm)],[c196,clause54]) ).
cnf(clause53,axiom,
( ~ general(X108,X107)
| ~ specific(X108,X107) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause53) ).
cnf(c200,plain,
~ general(skc7,skf8(skc8,skc7)),
inference(resolution,[status(thm)],[c195,clause53]) ).
cnf(clause57,axiom,
( ~ nonexistent(X116,X115)
| ~ existent(X116,X115) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause57) ).
cnf(c197,plain,
~ nonexistent(skc7,skf8(skc8,skc7)),
inference(resolution,[status(thm)],[c194,clause57]) ).
cnf(clause58,axiom,
( ~ nonliving(X118,X117)
| ~ animate(X118,X117) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause58) ).
cnf(c187,plain,
~ nonliving(skc7,skf8(skc8,skc7)),
inference(resolution,[status(thm)],[c182,clause58]) ).
cnf(clause51,axiom,
( ~ old(X104,X103)
| ~ young(X104,X103) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause51) ).
cnf(c178,plain,
~ old(skc7,skf8(skc8,skc7)),
inference(resolution,[status(thm)],[c174,clause51]) ).
cnf(c171,plain,
~ multiple(skc7,skf10(skc8,skc7)),
inference(resolution,[status(thm)],[c166,clause54]) ).
cnf(c168,plain,
~ general(skc7,skf10(skc8,skc7)),
inference(resolution,[status(thm)],[c165,clause53]) ).
cnf(c167,plain,
~ nonexistent(skc7,skf10(skc8,skc7)),
inference(resolution,[status(thm)],[c164,clause57]) ).
cnf(clause66,axiom,
( ~ member(X168,X166,X165)
| ~ member(X168,X167,X165)
| two(X168,X165)
| member(X168,skf11(X166,X167,X165,X168),X165)
| X166 = X167 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause66) ).
cnf(c157,plain,
~ nonliving(skc7,skf10(skc8,skc7)),
inference(resolution,[status(thm)],[c154,clause58]) ).
cnf(clause65,axiom,
( skf11(X159,X162,X158,X163) != X159
| ~ member(X160,X159,X161)
| ~ member(X160,X164,X161)
| two(X160,X161)
| X159 = X164 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause65) ).
cnf(c150,plain,
~ old(skc7,skf10(skc8,skc7)),
inference(resolution,[status(thm)],[c147,clause51]) ).
cnf(clause64,axiom,
( skf11(X153,X156,X152,X157) != X156
| ~ member(X154,X153,X155)
| ~ member(X154,X156,X155)
| two(X154,X155)
| X153 = X156 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause64) ).
cnf(c4,axiom,
( X150 != X149
| skf5(X150) = skf5(X149) ),
theory(equality) ).
cnf(clause63,axiom,
( ~ member(X147,X146,X145)
| ~ two(X147,X145)
| X146 = skf8(X145,X147)
| X146 = skf10(X145,X147) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause63) ).
cnf(c3,axiom,
( X144 != X143
| skf6(X144) = skf6(X143) ),
theory(equality) ).
cnf(transitivity,axiom,
( X137 != X138
| X138 != X139
| X137 = X139 ),
theory(equality) ).
cnf(clause62,axiom,
( skf10(X135,X134) != skf8(X135,X134)
| ~ two(X134,X135) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause62) ).
cnf(c56,axiom,
( X129 != X128
| ~ actual_world(X129)
| actual_world(X128) ),
theory(equality) ).
cnf(symmetry,axiom,
( X123 != X124
| X124 = X123 ),
theory(equality) ).
cnf(clause59,axiom,
( ~ be(X122,X120,X119,X121)
| X119 = X121 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause59) ).
cnf(c138,plain,
~ nonexistent(skc7,skc13),
inference(resolution,[status(thm)],[clause57,c96]) ).
cnf(c137,plain,
~ nonexistent(skc7,skc16),
inference(resolution,[status(thm)],[clause57,c82]) ).
cnf(c136,plain,
~ nonexistent(skc7,skc15),
inference(resolution,[status(thm)],[clause57,c115]) ).
cnf(clause56,axiom,
( ~ human(X114,X113)
| ~ nonhuman(X114,X113) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause56) ).
cnf(c135,plain,
~ human(skc7,skc14),
inference(resolution,[status(thm)],[clause56,c103]) ).
cnf(clause55,axiom,
( ~ living(X112,X111)
| ~ nonliving(X112,X111) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause55) ).
cnf(c134,plain,
~ living(skc7,skc13),
inference(resolution,[status(thm)],[clause55,c94]) ).
cnf(c133,plain,
~ living(skc7,skc15),
inference(resolution,[status(thm)],[clause55,c113]) ).
cnf(c132,plain,
~ living(skc7,skc16),
inference(resolution,[status(thm)],[clause55,c84]) ).
cnf(c131,plain,
~ multiple(skc7,skc12),
inference(resolution,[status(thm)],[clause54,c73]) ).
cnf(c130,plain,
~ multiple(skc7,skc15),
inference(resolution,[status(thm)],[clause54,c117]) ).
cnf(c129,plain,
~ multiple(skc7,skc14),
inference(resolution,[status(thm)],[clause54,c104]) ).
cnf(c128,plain,
~ multiple(skc7,skc16),
inference(resolution,[status(thm)],[clause54,c85]) ).
cnf(c127,plain,
~ multiple(skc7,skc13),
inference(resolution,[status(thm)],[clause54,c99]) ).
cnf(c126,plain,
~ general(skc7,skc16),
inference(resolution,[status(thm)],[clause53,c83]) ).
cnf(c125,plain,
~ general(skc7,skc15),
inference(resolution,[status(thm)],[clause53,c116]) ).
cnf(c124,plain,
~ general(skc7,skc13),
inference(resolution,[status(thm)],[clause53,c97]) ).
cnf(c123,plain,
~ general(skc7,skc12),
inference(resolution,[status(thm)],[clause53,c69]) ).
cnf(clause52,axiom,
( ~ male(X106,X105)
| ~ unisex(X106,X105) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause52) ).
cnf(c122,plain,
~ male(skc7,skc14),
inference(resolution,[status(thm)],[clause52,c106]) ).
cnf(c121,plain,
~ male(skc7,skc15),
inference(resolution,[status(thm)],[clause52,c111]) ).
cnf(c120,plain,
~ male(skc7,skc12),
inference(resolution,[status(thm)],[clause52,c68]) ).
cnf(c119,plain,
~ male(skc7,skc13),
inference(resolution,[status(thm)],[clause52,c92]) ).
cnf(c118,plain,
~ male(skc7,skc16),
inference(resolution,[status(thm)],[clause52,c87]) ).
cnf(clause50,axiom,
( ~ furniture(X102,X101)
| instrumentality(X102,X101) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause50) ).
cnf(clause49,axiom,
( ~ seat(X100,X99)
| furniture(X100,X99) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause49) ).
cnf(clause48,axiom,
( ~ frontseat(X98,X97)
| seat(X98,X97) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause48) ).
cnf(clause45,axiom,
( ~ hollywood_placename(X92,X91)
| placename(X92,X91) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause45) ).
cnf(clause25,axiom,
( ~ barrel(X52,X51)
| event(X52,X51) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause25) ).
cnf(clause23,axiom,
( ~ state(X48,X47)
| event(X48,X47) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause23) ).
cnf(clause18,axiom,
( ~ state(X38,X37)
| eventuality(X38,X37) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause18) ).
cnf(clause17,axiom,
( ~ two(X36,X35)
| group(X36,X35) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause17) ).
cnf(clause1,axiom,
~ member(X4,X3,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
cnf(clause68,negated_conjecture,
actual_world(skc7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause68) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : NLP144-1 : TPTP v8.1.2. Released v2.4.0.
% 0.12/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n025.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 13:47:38 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.85/1.03 % Version: 1.5
% 0.85/1.03 % SZS status Satisfiable
% 0.85/1.03 % SZS output start Saturation
% See solution above
% 0.85/1.04
% 0.85/1.04 % Initial clauses : 158
% 0.85/1.04 % Processed clauses : 520
% 0.85/1.04 % Factors computed : 26
% 0.85/1.04 % Resolvents computed: 479
% 0.85/1.04 % Tautologies deleted: 3
% 0.85/1.04 % Forward subsumed : 140
% 0.85/1.04 % Backward subsumed : 8
% 0.85/1.04 % -------- CPU Time ---------
% 0.85/1.04 % User time : 0.670 s
% 0.85/1.04 % System time : 0.013 s
% 0.85/1.04 % Total time : 0.683 s
%------------------------------------------------------------------------------