%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP024-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n007.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:40 EDT 2024
% Result : Satisfiable 1.00s 1.20s
% Output : Saturation 1.00s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(clause83,negated_conjecture,
accessible_world(skc8,skc10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause83) ).
cnf(clause88,negated_conjecture,
of(skc8,skc14,skc15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause88) ).
cnf(clause71,axiom,
( ~ accessible_world(X258,X257)
| ~ of(X258,X256,X255)
| of(X257,X256,X255) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause71) ).
cnf(c326,plain,
( ~ accessible_world(skc8,X425)
| of(X425,skc14,skc15) ),
inference(resolution,[status(thm)],[clause71,clause88]) ).
cnf(c513,plain,
of(skc10,skc14,skc15),
inference(resolution,[status(thm)],[c326,clause83]) ).
cnf(c34,axiom,
( X561 != X562
| X557 != X559
| X558 != X560
| ~ of(X561,X557,X558)
| of(X562,X559,X560) ),
theory(equality) ).
cnf(c606,plain,
( skc10 != X979
| skc14 != X978
| skc15 != X980
| of(X979,X978,X980) ),
inference(resolution,[status(thm)],[c34,c513]) ).
cnf(c882,plain,
( skc10 != X982
| skc14 != X981
| of(X982,X981,skc15) ),
inference(resolution,[status(thm)],[c606,reflexivity]) ).
cnf(c883,plain,
( skc10 != X983
| of(X983,skc14,skc15) ),
inference(resolution,[status(thm)],[c882,reflexivity]) ).
cnf(c605,plain,
( skc8 != X972
| skc14 != X971
| skc15 != X973
| of(X972,X971,X973) ),
inference(resolution,[status(thm)],[c34,clause88]) ).
cnf(c878,plain,
( skc8 != X976
| skc14 != X975
| of(X976,X975,skc15) ),
inference(resolution,[status(thm)],[c605,reflexivity]) ).
cnf(c880,plain,
( skc8 != X977
| of(X977,skc14,skc15) ),
inference(resolution,[status(thm)],[c878,reflexivity]) ).
cnf(clause89,negated_conjecture,
of(skc8,skc11,skc12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause89) ).
cnf(c325,plain,
( ~ accessible_world(skc8,X424)
| of(X424,skc11,skc12) ),
inference(resolution,[status(thm)],[clause71,clause89]) ).
cnf(c510,plain,
of(skc10,skc11,skc12),
inference(resolution,[status(thm)],[c325,clause83]) ).
cnf(c604,plain,
( skc10 != X967
| skc11 != X966
| skc12 != X968
| of(X967,X966,X968) ),
inference(resolution,[status(thm)],[c34,c510]) ).
cnf(c876,plain,
( skc10 != X970
| skc11 != X969
| of(X970,X969,skc12) ),
inference(resolution,[status(thm)],[c604,reflexivity]) ).
cnf(c877,plain,
( skc10 != X974
| of(X974,skc11,skc12) ),
inference(resolution,[status(thm)],[c876,reflexivity]) ).
cnf(c603,plain,
( skc8 != X961
| skc11 != X960
| skc12 != X962
| of(X961,X960,X962) ),
inference(resolution,[status(thm)],[c34,clause89]) ).
cnf(c873,plain,
( skc8 != X964
| skc11 != X963
| of(X964,X963,skc12) ),
inference(resolution,[status(thm)],[c603,reflexivity]) ).
cnf(c874,plain,
( skc8 != X965
| of(X965,skc11,skc12) ),
inference(resolution,[status(thm)],[c873,reflexivity]) ).
cnf(clause92,negated_conjecture,
theme(skc8,skc9,skc10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause92) ).
cnf(c33,axiom,
( X549 != X550
| X545 != X547
| X546 != X548
| ~ theme(X549,X545,X546)
| theme(X550,X547,X548) ),
theory(equality) ).
cnf(c598,plain,
( skc8 != X955
| skc9 != X954
| skc10 != X956
| theme(X955,X954,X956) ),
inference(resolution,[status(thm)],[c33,clause92]) ).
cnf(c870,plain,
( skc8 != X958
| skc9 != X957
| theme(X958,X957,skc10) ),
inference(resolution,[status(thm)],[c598,reflexivity]) ).
cnf(c871,plain,
( skc8 != X959
| theme(X959,skc9,skc10) ),
inference(resolution,[status(thm)],[c870,reflexivity]) ).
cnf(clause70,axiom,
( ~ accessible_world(X251,X250)
| ~ theme(X251,X249,X248)
| theme(X250,X249,X248) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause70) ).
cnf(c321,plain,
( ~ accessible_world(skc8,X419)
| theme(X419,skc9,skc10) ),
inference(resolution,[status(thm)],[clause70,clause92]) ).
cnf(c503,plain,
theme(skc10,skc9,skc10),
inference(resolution,[status(thm)],[c321,clause83]) ).
cnf(c597,plain,
( skc10 != X946
| skc9 != X945
| skc10 != X947
| theme(X946,X945,X947) ),
inference(resolution,[status(thm)],[c33,c503]) ).
cnf(c865,plain,
( skc10 != X951
| skc9 != X952
| theme(X951,X952,skc10) ),
inference(resolution,[status(thm)],[c597,reflexivity]) ).
cnf(c868,plain,
( skc10 != X953
| theme(X953,skc9,skc10) ),
inference(resolution,[status(thm)],[c865,reflexivity]) ).
cnf(c864,plain,
( skc10 != X949
| skc9 != X948
| theme(X949,X948,X949) ),
inference(factor,[status(thm)],[c597]) ).
cnf(c866,plain,
( skc10 != X950
| theme(X950,skc9,X950) ),
inference(resolution,[status(thm)],[c864,reflexivity]) ).
cnf(clause90,negated_conjecture,
agent(skc8,skc9,skc12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause90) ).
cnf(c32,axiom,
( X539 != X540
| X535 != X537
| X536 != X538
| ~ agent(X539,X535,X536)
| agent(X540,X537,X538) ),
theory(equality) ).
cnf(c593,plain,
( skc8 != X940
| skc9 != X939
| skc12 != X941
| agent(X940,X939,X941) ),
inference(resolution,[status(thm)],[c32,clause90]) ).
cnf(c861,plain,
( skc8 != X942
| skc9 != X943
| agent(X942,X943,skc12) ),
inference(resolution,[status(thm)],[c593,reflexivity]) ).
cnf(c862,plain,
( skc8 != X944
| agent(X944,skc9,skc12) ),
inference(resolution,[status(thm)],[c861,reflexivity]) ).
cnf(clause69,axiom,
( ~ accessible_world(X245,X244)
| ~ agent(X245,X243,X242)
| agent(X244,X243,X242) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause69) ).
cnf(c315,plain,
( ~ accessible_world(skc8,X418)
| agent(X418,skc9,skc12) ),
inference(resolution,[status(thm)],[clause69,clause90]) ).
cnf(c501,plain,
agent(skc10,skc9,skc12),
inference(resolution,[status(thm)],[c315,clause83]) ).
cnf(c592,plain,
( skc10 != X934
| skc9 != X933
| skc12 != X935
| agent(X934,X933,X935) ),
inference(resolution,[status(thm)],[c32,c501]) ).
cnf(c858,plain,
( skc10 != X936
| skc9 != X937
| agent(X936,X937,skc12) ),
inference(resolution,[status(thm)],[c592,reflexivity]) ).
cnf(c859,plain,
( skc10 != X938
| agent(X938,skc9,skc12) ),
inference(resolution,[status(thm)],[c858,reflexivity]) ).
cnf(clause91,negated_conjecture,
agent(skc10,skc13,skc12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause91) ).
cnf(c591,plain,
( skc10 != X928
| skc13 != X927
| skc12 != X929
| agent(X928,X927,X929) ),
inference(resolution,[status(thm)],[c32,clause91]) ).
cnf(c855,plain,
( skc10 != X931
| skc13 != X930
| agent(X931,X930,skc12) ),
inference(resolution,[status(thm)],[c591,reflexivity]) ).
cnf(c856,plain,
( skc10 != X932
| agent(X932,skc13,skc12) ),
inference(resolution,[status(thm)],[c855,reflexivity]) ).
cnf(clause85,negated_conjecture,
present(skc8,skc9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause85) ).
cnf(c31,axiom,
( X526 != X529
| X528 != X527
| ~ present(X526,X528)
| present(X529,X527) ),
theory(equality) ).
cnf(c587,plain,
( skc8 != X925
| skc9 != X924
| present(X925,X924) ),
inference(resolution,[status(thm)],[c31,clause85]) ).
cnf(c853,plain,
( skc8 != X926
| present(X926,skc9) ),
inference(resolution,[status(thm)],[c587,reflexivity]) ).
cnf(clause78,negated_conjecture,
present(skc10,skc13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause78) ).
cnf(c586,plain,
( skc10 != X922
| skc13 != X921
| present(X922,X921) ),
inference(resolution,[status(thm)],[c31,clause78]) ).
cnf(c851,plain,
( skc10 != X923
| present(X923,skc13) ),
inference(resolution,[status(thm)],[c586,reflexivity]) ).
cnf(clause46,axiom,
( ~ accessible_world(X122,X121)
| ~ present(X122,X120)
| present(X121,X120) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause46) ).
cnf(c187,plain,
( ~ accessible_world(skc8,X189)
| present(X189,skc9) ),
inference(resolution,[status(thm)],[clause46,clause85]) ).
cnf(c241,plain,
present(skc10,skc9),
inference(resolution,[status(thm)],[c187,clause83]) ).
cnf(c585,plain,
( skc10 != X919
| skc9 != X918
| present(X919,X918) ),
inference(resolution,[status(thm)],[c31,c241]) ).
cnf(c849,plain,
( skc10 != X920
| present(X920,skc9) ),
inference(resolution,[status(thm)],[c585,reflexivity]) ).
cnf(c30,axiom,
( X516 != X519
| X518 != X517
| ~ accessible_world(X516,X518)
| accessible_world(X519,X517) ),
theory(equality) ).
cnf(c580,plain,
( skc8 != X916
| skc10 != X915
| accessible_world(X916,X915) ),
inference(resolution,[status(thm)],[c30,clause83]) ).
cnf(c847,plain,
( skc8 != X917
| accessible_world(X917,skc10) ),
inference(resolution,[status(thm)],[c580,reflexivity]) ).
cnf(clause75,negated_conjecture,
man(skc8,skc15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause75) ).
cnf(clause31,axiom,
( ~ man(X64,X63)
| male(X64,X63) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
cnf(c94,plain,
male(skc8,skc15),
inference(resolution,[status(thm)],[clause31,clause75]) ).
cnf(c29,axiom,
( X508 != X511
| X510 != X509
| ~ male(X508,X510)
| male(X511,X509) ),
theory(equality) ).
cnf(c576,plain,
( skc8 != X913
| skc15 != X912
| male(X913,X912) ),
inference(resolution,[status(thm)],[c29,c94]) ).
cnf(c845,plain,
( skc8 != X914
| male(X914,skc15) ),
inference(resolution,[status(thm)],[c576,reflexivity]) ).
cnf(clause67,axiom,
( ~ accessible_world(X234,X233)
| ~ man(X234,X232)
| man(X233,X232) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause67) ).
cnf(c304,plain,
( ~ accessible_world(skc8,X361)
| man(X361,skc15) ),
inference(resolution,[status(thm)],[clause67,clause75]) ).
cnf(c466,plain,
man(skc10,skc15),
inference(resolution,[status(thm)],[c304,clause83]) ).
cnf(c467,plain,
male(skc10,skc15),
inference(resolution,[status(thm)],[c466,clause31]) ).
cnf(c575,plain,
( skc10 != X910
| skc15 != X909
| male(X910,X909) ),
inference(resolution,[status(thm)],[c29,c467]) ).
cnf(c843,plain,
( skc10 != X911
| male(X911,skc15) ),
inference(resolution,[status(thm)],[c575,reflexivity]) ).
cnf(c28,axiom,
( X500 != X503
| X502 != X501
| ~ man(X500,X502)
| man(X503,X501) ),
theory(equality) ).
cnf(c571,plain,
( skc10 != X906
| skc15 != X907
| man(X906,X907) ),
inference(resolution,[status(thm)],[c28,c466]) ).
cnf(c841,plain,
( skc10 != X908
| man(X908,skc15) ),
inference(resolution,[status(thm)],[c571,reflexivity]) ).
cnf(c570,plain,
( skc8 != X903
| skc15 != X904
| man(X903,X904) ),
inference(resolution,[status(thm)],[c28,clause75]) ).
cnf(c839,plain,
( skc8 != X905
| man(X905,skc15) ),
inference(resolution,[status(thm)],[c570,reflexivity]) ).
cnf(clause87,negated_conjecture,
vincent_forename(skc8,skc14),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause87) ).
cnf(c27,axiom,
( X491 != X494
| X493 != X492
| ~ vincent_forename(X491,X493)
| vincent_forename(X494,X492) ),
theory(equality) ).
cnf(c565,plain,
( skc8 != X901
| skc14 != X900
| vincent_forename(X901,X900) ),
inference(resolution,[status(thm)],[c27,clause87]) ).
cnf(c837,plain,
( skc8 != X902
| vincent_forename(X902,skc14) ),
inference(resolution,[status(thm)],[c565,reflexivity]) ).
cnf(clause66,axiom,
( ~ accessible_world(X229,X228)
| ~ vincent_forename(X229,X227)
| vincent_forename(X228,X227) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause66) ).
cnf(c301,plain,
( ~ accessible_world(skc8,X356)
| vincent_forename(X356,skc14) ),
inference(resolution,[status(thm)],[clause66,clause87]) ).
cnf(c457,plain,
vincent_forename(skc10,skc14),
inference(resolution,[status(thm)],[c301,clause83]) ).
cnf(c564,plain,
( skc10 != X898
| skc14 != X897
| vincent_forename(X898,X897) ),
inference(resolution,[status(thm)],[c27,c457]) ).
cnf(c835,plain,
( skc10 != X899
| vincent_forename(X899,skc14) ),
inference(resolution,[status(thm)],[c564,reflexivity]) ).
cnf(clause77,negated_conjecture,
woman(skc8,skc12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause77) ).
cnf(clause28,axiom,
( ~ woman(X58,X57)
| female(X58,X57) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
cnf(c85,plain,
female(skc8,skc12),
inference(resolution,[status(thm)],[clause28,clause77]) ).
cnf(c26,axiom,
( X481 != X484
| X483 != X482
| ~ female(X481,X483)
| female(X484,X482) ),
theory(equality) ).
cnf(c559,plain,
( skc8 != X895
| skc12 != X894
| female(X895,X894) ),
inference(resolution,[status(thm)],[c26,c85]) ).
cnf(c833,plain,
( skc8 != X896
| female(X896,skc12) ),
inference(resolution,[status(thm)],[c559,reflexivity]) ).
cnf(clause56,axiom,
( ~ accessible_world(X181,X180)
| ~ woman(X181,X179)
| woman(X180,X179) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause56) ).
cnf(c235,plain,
( ~ accessible_world(skc8,X260)
| woman(X260,skc12) ),
inference(resolution,[status(thm)],[clause56,clause77]) ).
cnf(c329,plain,
woman(skc10,skc12),
inference(resolution,[status(thm)],[c235,clause83]) ).
cnf(c330,plain,
female(skc10,skc12),
inference(resolution,[status(thm)],[c329,clause28]) ).
cnf(c558,plain,
( skc10 != X892
| skc12 != X891
| female(X892,X891) ),
inference(resolution,[status(thm)],[c26,c330]) ).
cnf(c831,plain,
( skc10 != X893
| female(X893,skc12) ),
inference(resolution,[status(thm)],[c558,reflexivity]) ).
cnf(clause27,axiom,
( ~ human_person(X56,X55)
| animate(X56,X55) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
cnf(clause30,axiom,
( ~ man(X62,X61)
| human_person(X62,X61) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
cnf(c87,plain,
human_person(skc8,skc15),
inference(resolution,[status(thm)],[clause30,clause75]) ).
cnf(c88,plain,
animate(skc8,skc15),
inference(resolution,[status(thm)],[c87,clause27]) ).
cnf(c25,axiom,
( X473 != X476
| X475 != X474
| ~ animate(X473,X475)
| animate(X476,X474) ),
theory(equality) ).
cnf(c554,plain,
( skc8 != X888
| skc15 != X889
| animate(X888,X889) ),
inference(resolution,[status(thm)],[c25,c88]) ).
cnf(c829,plain,
( skc8 != X890
| animate(X890,skc15) ),
inference(resolution,[status(thm)],[c554,reflexivity]) ).
cnf(clause18,axiom,
( ~ woman(X38,X37)
| human_person(X38,X37) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
cnf(c332,plain,
human_person(skc10,skc12),
inference(resolution,[status(thm)],[c329,clause18]) ).
cnf(c338,plain,
animate(skc10,skc12),
inference(resolution,[status(thm)],[c332,clause27]) ).
cnf(c553,plain,
( skc10 != X885
| skc12 != X886
| animate(X885,X886) ),
inference(resolution,[status(thm)],[c25,c338]) ).
cnf(c827,plain,
( skc10 != X887
| animate(X887,skc12) ),
inference(resolution,[status(thm)],[c553,reflexivity]) ).
cnf(clause57,axiom,
( ~ accessible_world(X186,X185)
| ~ human_person(X186,X184)
| human_person(X185,X184) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause57) ).
cnf(c239,plain,
( ~ accessible_world(skc8,X274)
| human_person(X274,skc15) ),
inference(resolution,[status(thm)],[clause57,c87]) ).
cnf(c358,plain,
human_person(skc10,skc15),
inference(resolution,[status(thm)],[c239,clause83]) ).
cnf(c360,plain,
animate(skc10,skc15),
inference(resolution,[status(thm)],[c358,clause27]) ).
cnf(c552,plain,
( skc10 != X882
| skc15 != X883
| animate(X882,X883) ),
inference(resolution,[status(thm)],[c25,c360]) ).
cnf(c825,plain,
( skc10 != X884
| animate(X884,skc15) ),
inference(resolution,[status(thm)],[c552,reflexivity]) ).
cnf(c74,plain,
human_person(skc8,skc12),
inference(resolution,[status(thm)],[clause18,clause77]) ).
cnf(c84,plain,
animate(skc8,skc12),
inference(resolution,[status(thm)],[clause27,c74]) ).
cnf(c551,plain,
( skc8 != X879
| skc12 != X880
| animate(X879,X880) ),
inference(resolution,[status(thm)],[c25,c84]) ).
cnf(c823,plain,
( skc8 != X881
| animate(X881,skc12) ),
inference(resolution,[status(thm)],[c551,reflexivity]) ).
cnf(clause26,axiom,
( ~ human_person(X54,X53)
| human(X54,X53) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
cnf(c89,plain,
human(skc8,skc15),
inference(resolution,[status(thm)],[c87,clause26]) ).
cnf(c24,axiom,
( X464 != X467
| X466 != X465
| ~ human(X464,X466)
| human(X467,X465) ),
theory(equality) ).
cnf(c547,plain,
( skc8 != X876
| skc15 != X877
| human(X876,X877) ),
inference(resolution,[status(thm)],[c24,c89]) ).
cnf(c821,plain,
( skc8 != X878
| human(X878,skc15) ),
inference(resolution,[status(thm)],[c547,reflexivity]) ).
cnf(c361,plain,
human(skc10,skc15),
inference(resolution,[status(thm)],[c358,clause26]) ).
cnf(c546,plain,
( skc10 != X873
| skc15 != X874
| human(X873,X874) ),
inference(resolution,[status(thm)],[c24,c361]) ).
cnf(c819,plain,
( skc10 != X875
| human(X875,skc15) ),
inference(resolution,[status(thm)],[c546,reflexivity]) ).
cnf(c339,plain,
human(skc10,skc12),
inference(resolution,[status(thm)],[c332,clause26]) ).
cnf(c545,plain,
( skc10 != X870
| skc12 != X871
| human(X870,X871) ),
inference(resolution,[status(thm)],[c24,c339]) ).
cnf(c817,plain,
( skc10 != X872
| human(X872,skc12) ),
inference(resolution,[status(thm)],[c545,reflexivity]) ).
cnf(c83,plain,
human(skc8,skc12),
inference(resolution,[status(thm)],[clause26,c74]) ).
cnf(c544,plain,
( skc8 != X867
| skc12 != X868
| human(X867,X868) ),
inference(resolution,[status(thm)],[c24,c83]) ).
cnf(c815,plain,
( skc8 != X869
| human(X869,skc12) ),
inference(resolution,[status(thm)],[c544,reflexivity]) ).
cnf(clause25,axiom,
( ~ organism(X52,X51)
| living(X52,X51) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
cnf(clause19,axiom,
( ~ human_person(X40,X39)
| organism(X40,X39) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
cnf(c90,plain,
organism(skc8,skc15),
inference(resolution,[status(thm)],[c87,clause19]) ).
cnf(c93,plain,
living(skc8,skc15),
inference(resolution,[status(thm)],[c90,clause25]) ).
cnf(c23,axiom,
( X454 != X457
| X456 != X455
| ~ living(X454,X456)
| living(X457,X455) ),
theory(equality) ).
cnf(c539,plain,
( skc8 != X865
| skc15 != X864
| living(X865,X864) ),
inference(resolution,[status(thm)],[c23,c93]) ).
cnf(c813,plain,
( skc8 != X866
| living(X866,skc15) ),
inference(resolution,[status(thm)],[c539,reflexivity]) ).
cnf(c75,plain,
organism(skc8,skc12),
inference(resolution,[status(thm)],[c74,clause19]) ).
cnf(c82,plain,
living(skc8,skc12),
inference(resolution,[status(thm)],[clause25,c75]) ).
cnf(c538,plain,
( skc8 != X862
| skc12 != X861
| living(X862,X861) ),
inference(resolution,[status(thm)],[c23,c82]) ).
cnf(c811,plain,
( skc8 != X863
| living(X863,skc12) ),
inference(resolution,[status(thm)],[c538,reflexivity]) ).
cnf(c340,plain,
organism(skc10,skc12),
inference(resolution,[status(thm)],[c332,clause19]) ).
cnf(c346,plain,
living(skc10,skc12),
inference(resolution,[status(thm)],[c340,clause25]) ).
cnf(c537,plain,
( skc10 != X859
| skc12 != X858
| living(X859,X858) ),
inference(resolution,[status(thm)],[c23,c346]) ).
cnf(c809,plain,
( skc10 != X860
| living(X860,skc12) ),
inference(resolution,[status(thm)],[c537,reflexivity]) ).
cnf(c362,plain,
organism(skc10,skc15),
inference(resolution,[status(thm)],[c358,clause19]) ).
cnf(c370,plain,
living(skc10,skc15),
inference(resolution,[status(thm)],[c362,clause25]) ).
cnf(c536,plain,
( skc10 != X856
| skc15 != X855
| living(X856,X855) ),
inference(resolution,[status(thm)],[c23,c370]) ).
cnf(c807,plain,
( skc10 != X857
| living(X857,skc15) ),
inference(resolution,[status(thm)],[c536,reflexivity]) ).
cnf(clause24,axiom,
( ~ organism(X50,X49)
| impartial(X50,X49) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
cnf(c81,plain,
impartial(skc8,skc12),
inference(resolution,[status(thm)],[clause24,c75]) ).
cnf(c22,axiom,
( X446 != X449
| X448 != X447
| ~ impartial(X446,X448)
| impartial(X449,X447) ),
theory(equality) ).
cnf(c532,plain,
( skc8 != X852
| skc12 != X853
| impartial(X852,X853) ),
inference(resolution,[status(thm)],[c22,c81]) ).
cnf(c805,plain,
( skc8 != X854
| impartial(X854,skc12) ),
inference(resolution,[status(thm)],[c532,reflexivity]) ).
cnf(c367,plain,
impartial(skc10,skc15),
inference(resolution,[status(thm)],[c362,clause24]) ).
cnf(c531,plain,
( skc10 != X849
| skc15 != X850
| impartial(X849,X850) ),
inference(resolution,[status(thm)],[c22,c367]) ).
cnf(c803,plain,
( skc10 != X851
| impartial(X851,skc15) ),
inference(resolution,[status(thm)],[c531,reflexivity]) ).
cnf(c343,plain,
impartial(skc10,skc12),
inference(resolution,[status(thm)],[c340,clause24]) ).
cnf(c530,plain,
( skc10 != X846
| skc12 != X847
| impartial(X846,X847) ),
inference(resolution,[status(thm)],[c22,c343]) ).
cnf(c801,plain,
( skc10 != X848
| impartial(X848,skc12) ),
inference(resolution,[status(thm)],[c530,reflexivity]) ).
cnf(c91,plain,
impartial(skc8,skc15),
inference(resolution,[status(thm)],[c90,clause24]) ).
cnf(c529,plain,
( skc8 != X843
| skc15 != X844
| impartial(X843,X844) ),
inference(resolution,[status(thm)],[c22,c91]) ).
cnf(c799,plain,
( skc8 != X845
| impartial(X845,skc15) ),
inference(resolution,[status(thm)],[c529,reflexivity]) ).
cnf(clause23,axiom,
( ~ entity(X48,X47)
| existent(X48,X47) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
cnf(clause20,axiom,
( ~ organism(X42,X41)
| entity(X42,X41) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
cnf(c92,plain,
entity(skc8,skc15),
inference(resolution,[status(thm)],[c90,clause20]) ).
cnf(c97,plain,
existent(skc8,skc15),
inference(resolution,[status(thm)],[c92,clause23]) ).
cnf(c21,axiom,
( X437 != X440
| X439 != X438
| ~ existent(X437,X439)
| existent(X440,X438) ),
theory(equality) ).
cnf(c525,plain,
( skc8 != X840
| skc15 != X841
| existent(X840,X841) ),
inference(resolution,[status(thm)],[c21,c97]) ).
cnf(c797,plain,
( skc8 != X842
| existent(X842,skc15) ),
inference(resolution,[status(thm)],[c525,reflexivity]) ).
cnf(c76,plain,
entity(skc8,skc12),
inference(resolution,[status(thm)],[clause20,c75]) ).
cnf(c80,plain,
existent(skc8,skc12),
inference(resolution,[status(thm)],[clause23,c76]) ).
cnf(c524,plain,
( skc8 != X837
| skc12 != X838
| existent(X837,X838) ),
inference(resolution,[status(thm)],[c21,c80]) ).
cnf(c795,plain,
( skc8 != X839
| existent(X839,skc12) ),
inference(resolution,[status(thm)],[c524,reflexivity]) ).
cnf(c344,plain,
entity(skc10,skc12),
inference(resolution,[status(thm)],[c340,clause20]) ).
cnf(c353,plain,
existent(skc10,skc12),
inference(resolution,[status(thm)],[c344,clause23]) ).
cnf(c523,plain,
( skc10 != X834
| skc12 != X835
| existent(X834,X835) ),
inference(resolution,[status(thm)],[c21,c353]) ).
cnf(c793,plain,
( skc10 != X836
| existent(X836,skc12) ),
inference(resolution,[status(thm)],[c523,reflexivity]) ).
cnf(c368,plain,
entity(skc10,skc15),
inference(resolution,[status(thm)],[c362,clause20]) ).
cnf(c375,plain,
existent(skc10,skc15),
inference(resolution,[status(thm)],[c368,clause23]) ).
cnf(c522,plain,
( skc10 != X831
| skc15 != X832
| existent(X831,X832) ),
inference(resolution,[status(thm)],[c21,c375]) ).
cnf(c791,plain,
( skc10 != X833
| existent(X833,skc15) ),
inference(resolution,[status(thm)],[c522,reflexivity]) ).
cnf(c20,axiom,
( X427 != X430
| X429 != X428
| ~ entity(X427,X429)
| entity(X430,X428) ),
theory(equality) ).
cnf(c519,plain,
( skc8 != X828
| skc15 != X829
| entity(X828,X829) ),
inference(resolution,[status(thm)],[c20,c92]) ).
cnf(c789,plain,
( skc8 != X830
| entity(X830,skc15) ),
inference(resolution,[status(thm)],[c519,reflexivity]) ).
cnf(c518,plain,
( skc10 != X825
| skc12 != X826
| entity(X825,X826) ),
inference(resolution,[status(thm)],[c20,c344]) ).
cnf(c787,plain,
( skc10 != X827
| entity(X827,skc12) ),
inference(resolution,[status(thm)],[c518,reflexivity]) ).
cnf(clause72,axiom,
( ~ forename(X264,X263)
| ~ of(X264,X262,X261)
| ~ forename(X264,X262)
| ~ of(X264,X263,X261)
| ~ entity(X264,X261)
| X262 = X263 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause72) ).
cnf(c515,plain,
( ~ forename(skc10,skc14)
| ~ of(skc10,X824,skc15)
| ~ forename(skc10,X824)
| ~ entity(skc10,skc15)
| X824 = skc14 ),
inference(resolution,[status(thm)],[c513,clause72]) ).
cnf(c517,plain,
( skc10 != X821
| skc15 != X822
| entity(X821,X822) ),
inference(resolution,[status(thm)],[c20,c368]) ).
cnf(c784,plain,
( skc10 != X823
| entity(X823,skc15) ),
inference(resolution,[status(thm)],[c517,reflexivity]) ).
cnf(c516,plain,
( skc8 != X817
| skc12 != X818
| entity(X817,X818) ),
inference(resolution,[status(thm)],[c20,c76]) ).
cnf(c781,plain,
( skc8 != X820
| entity(X820,skc12) ),
inference(resolution,[status(thm)],[c516,reflexivity]) ).
cnf(c512,plain,
( ~ forename(skc10,skc11)
| ~ of(skc10,X819,skc12)
| ~ forename(skc10,X819)
| ~ entity(skc10,skc12)
| X819 = skc11 ),
inference(resolution,[status(thm)],[c510,clause72]) ).
cnf(c19,axiom,
( X420 != X423
| X422 != X421
| ~ organism(X420,X422)
| organism(X423,X421) ),
theory(equality) ).
cnf(c509,plain,
( skc10 != X813
| skc12 != X814
| organism(X813,X814) ),
inference(resolution,[status(thm)],[c19,c340]) ).
cnf(c778,plain,
( skc10 != X816
| organism(X816,skc12) ),
inference(resolution,[status(thm)],[c509,reflexivity]) ).
cnf(c508,plain,
( skc8 != X811
| skc15 != X812
| organism(X811,X812) ),
inference(resolution,[status(thm)],[c19,c90]) ).
cnf(c777,plain,
( skc8 != X815
| organism(X815,skc15) ),
inference(resolution,[status(thm)],[c508,reflexivity]) ).
cnf(c507,plain,
( skc10 != X808
| skc15 != X809
| organism(X808,X809) ),
inference(resolution,[status(thm)],[c19,c362]) ).
cnf(c775,plain,
( skc10 != X810
| organism(X810,skc15) ),
inference(resolution,[status(thm)],[c507,reflexivity]) ).
cnf(clause73,axiom,
( ~ theme(X265,X268,X267)
| ~ desire_want(X265,X268)
| ~ proposition(X265,X267)
| ~ proposition(X265,X266)
| ~ desire_want(X265,X269)
| ~ theme(X265,X269,X266)
| X266 = X267 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause73) ).
cnf(c504,plain,
( ~ theme(skc10,X807,X806)
| ~ desire_want(skc10,X807)
| ~ proposition(skc10,X806)
| ~ proposition(skc10,skc10)
| ~ desire_want(skc10,skc9)
| skc10 = X806 ),
inference(resolution,[status(thm)],[c503,clause73]) ).
cnf(c506,plain,
( skc8 != X803
| skc12 != X804
| organism(X803,X804) ),
inference(resolution,[status(thm)],[c19,c75]) ).
cnf(c772,plain,
( skc8 != X805
| organism(X805,skc12) ),
inference(resolution,[status(thm)],[c506,reflexivity]) ).
cnf(c18,axiom,
( X413 != X416
| X415 != X414
| ~ human_person(X413,X415)
| human_person(X416,X414) ),
theory(equality) ).
cnf(c500,plain,
( skc8 != X801
| skc12 != X800
| human_person(X801,X800) ),
inference(resolution,[status(thm)],[c18,c74]) ).
cnf(c770,plain,
( skc8 != X802
| human_person(X802,skc12) ),
inference(resolution,[status(thm)],[c500,reflexivity]) ).
cnf(c499,plain,
( skc10 != X798
| skc12 != X797
| human_person(X798,X797) ),
inference(resolution,[status(thm)],[c18,c332]) ).
cnf(c768,plain,
( skc10 != X799
| human_person(X799,skc12) ),
inference(resolution,[status(thm)],[c499,reflexivity]) ).
cnf(c498,plain,
( skc10 != X795
| skc15 != X794
| human_person(X795,X794) ),
inference(resolution,[status(thm)],[c18,c358]) ).
cnf(c766,plain,
( skc10 != X796
| human_person(X796,skc15) ),
inference(resolution,[status(thm)],[c498,reflexivity]) ).
cnf(c497,plain,
( skc8 != X792
| skc15 != X791
| human_person(X792,X791) ),
inference(resolution,[status(thm)],[c18,c87]) ).
cnf(c764,plain,
( skc8 != X793
| human_person(X793,skc15) ),
inference(resolution,[status(thm)],[c497,reflexivity]) ).
cnf(c17,axiom,
( X404 != X407
| X406 != X405
| ~ woman(X404,X406)
| woman(X407,X405) ),
theory(equality) ).
cnf(c496,plain,
( skc10 != X788
| skc12 != X789
| woman(X788,X789) ),
inference(resolution,[status(thm)],[c17,c329]) ).
cnf(c762,plain,
( skc10 != X790
| woman(X790,skc12) ),
inference(resolution,[status(thm)],[c496,reflexivity]) ).
cnf(c495,plain,
( skc8 != X785
| skc12 != X786
| woman(X785,X786) ),
inference(resolution,[status(thm)],[c17,clause77]) ).
cnf(c760,plain,
( skc8 != X787
| woman(X787,skc12) ),
inference(resolution,[status(thm)],[c495,reflexivity]) ).
cnf(clause81,negated_conjecture,
mia_forename(skc8,skc11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause81) ).
cnf(c16,axiom,
( X395 != X398
| X397 != X396
| ~ mia_forename(X395,X397)
| mia_forename(X398,X396) ),
theory(equality) ).
cnf(c494,plain,
( skc8 != X782
| skc11 != X783
| mia_forename(X782,X783) ),
inference(resolution,[status(thm)],[c16,clause81]) ).
cnf(c758,plain,
( skc8 != X784
| mia_forename(X784,skc11) ),
inference(resolution,[status(thm)],[c494,reflexivity]) ).
cnf(clause55,axiom,
( ~ accessible_world(X176,X175)
| ~ mia_forename(X176,X174)
| mia_forename(X175,X174) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause55) ).
cnf(c230,plain,
( ~ accessible_world(skc8,X254)
| mia_forename(X254,skc11) ),
inference(resolution,[status(thm)],[clause55,clause81]) ).
cnf(c324,plain,
mia_forename(skc10,skc11),
inference(resolution,[status(thm)],[c230,clause83]) ).
cnf(c493,plain,
( skc10 != X779
| skc11 != X780
| mia_forename(X779,X780) ),
inference(resolution,[status(thm)],[c16,c324]) ).
cnf(c756,plain,
( skc10 != X781
| mia_forename(X781,skc11) ),
inference(resolution,[status(thm)],[c493,reflexivity]) ).
cnf(clause15,axiom,
( ~ forename(X32,X31)
| relname(X32,X31) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
cnf(clause86,negated_conjecture,
forename(skc8,skc14),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause86) ).
cnf(clause53,axiom,
( ~ accessible_world(X164,X163)
| ~ forename(X164,X162)
| forename(X163,X162) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause53) ).
cnf(c221,plain,
( ~ accessible_world(skc8,X246)
| forename(X246,skc14) ),
inference(resolution,[status(thm)],[clause53,clause86]) ).
cnf(c316,plain,
forename(skc10,skc14),
inference(resolution,[status(thm)],[c221,clause83]) ).
cnf(c317,plain,
relname(skc10,skc14),
inference(resolution,[status(thm)],[c316,clause15]) ).
cnf(c15,axiom,
( X386 != X389
| X388 != X387
| ~ relname(X386,X388)
| relname(X389,X387) ),
theory(equality) ).
cnf(c492,plain,
( skc10 != X777
| skc14 != X776
| relname(X777,X776) ),
inference(resolution,[status(thm)],[c15,c317]) ).
cnf(c754,plain,
( skc10 != X778
| relname(X778,skc14) ),
inference(resolution,[status(thm)],[c492,reflexivity]) ).
cnf(c58,plain,
relname(skc8,skc14),
inference(resolution,[status(thm)],[clause15,clause86]) ).
cnf(c491,plain,
( skc8 != X774
| skc14 != X773
| relname(X774,X773) ),
inference(resolution,[status(thm)],[c15,c58]) ).
cnf(c752,plain,
( skc8 != X775
| relname(X775,skc14) ),
inference(resolution,[status(thm)],[c491,reflexivity]) ).
cnf(clause80,negated_conjecture,
forename(skc8,skc11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause80) ).
cnf(c220,plain,
( ~ accessible_world(skc8,X241)
| forename(X241,skc11) ),
inference(resolution,[status(thm)],[clause53,clause80]) ).
cnf(c309,plain,
forename(skc10,skc11),
inference(resolution,[status(thm)],[c220,clause83]) ).
cnf(c310,plain,
relname(skc10,skc11),
inference(resolution,[status(thm)],[c309,clause15]) ).
cnf(c490,plain,
( skc10 != X771
| skc11 != X770
| relname(X771,X770) ),
inference(resolution,[status(thm)],[c15,c310]) ).
cnf(c750,plain,
( skc10 != X772
| relname(X772,skc11) ),
inference(resolution,[status(thm)],[c490,reflexivity]) ).
cnf(c57,plain,
relname(skc8,skc11),
inference(resolution,[status(thm)],[clause15,clause80]) ).
cnf(c489,plain,
( skc8 != X768
| skc11 != X767
| relname(X768,X767) ),
inference(resolution,[status(thm)],[c15,c57]) ).
cnf(c748,plain,
( skc8 != X769
| relname(X769,skc11) ),
inference(resolution,[status(thm)],[c489,reflexivity]) ).
cnf(c14,axiom,
( X377 != X380
| X379 != X378
| ~ forename(X377,X379)
| forename(X380,X378) ),
theory(equality) ).
cnf(c488,plain,
( skc10 != X765
| skc14 != X764
| forename(X765,X764) ),
inference(resolution,[status(thm)],[c14,c316]) ).
cnf(c746,plain,
( skc10 != X766
| forename(X766,skc14) ),
inference(resolution,[status(thm)],[c488,reflexivity]) ).
cnf(c487,plain,
( skc8 != X762
| skc14 != X761
| forename(X762,X761) ),
inference(resolution,[status(thm)],[c14,clause86]) ).
cnf(c744,plain,
( skc8 != X763
| forename(X763,skc14) ),
inference(resolution,[status(thm)],[c487,reflexivity]) ).
cnf(c486,plain,
( skc8 != X759
| skc11 != X758
| forename(X759,X758) ),
inference(resolution,[status(thm)],[c14,clause80]) ).
cnf(c742,plain,
( skc8 != X760
| forename(X760,skc11) ),
inference(resolution,[status(thm)],[c486,reflexivity]) ).
cnf(c485,plain,
( skc10 != X756
| skc11 != X755
| forename(X756,X755) ),
inference(resolution,[status(thm)],[c14,c309]) ).
cnf(c740,plain,
( skc10 != X757
| forename(X757,skc11) ),
inference(resolution,[status(thm)],[c485,reflexivity]) ).
cnf(clause82,negated_conjecture,
proposition(skc8,skc10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause82) ).
cnf(clause9,axiom,
( ~ proposition(X20,X19)
| relation(X20,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
cnf(c50,plain,
relation(skc8,skc10),
inference(resolution,[status(thm)],[clause9,clause82]) ).
cnf(clause10,axiom,
( ~ relation(X22,X21)
| abstraction(X22,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(c51,plain,
abstraction(skc8,skc10),
inference(resolution,[status(thm)],[clause10,c50]) ).
cnf(clause13,axiom,
( ~ abstraction(X28,X27)
| general(X28,X27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
cnf(c55,plain,
general(skc8,skc10),
inference(resolution,[status(thm)],[clause13,c51]) ).
cnf(c13,axiom,
( X368 != X371
| X370 != X369
| ~ general(X368,X370)
| general(X371,X369) ),
theory(equality) ).
cnf(c484,plain,
( skc8 != X752
| skc10 != X753
| general(X752,X753) ),
inference(resolution,[status(thm)],[c13,c55]) ).
cnf(c738,plain,
( skc8 != X754
| general(X754,skc10) ),
inference(resolution,[status(thm)],[c484,reflexivity]) ).
cnf(clause16,axiom,
( ~ relname(X34,X33)
| relation(X34,X33) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(c60,plain,
relation(skc8,skc14),
inference(resolution,[status(thm)],[clause16,c58]) ).
cnf(c62,plain,
abstraction(skc8,skc14),
inference(resolution,[status(thm)],[c60,clause10]) ).
cnf(c70,plain,
general(skc8,skc14),
inference(resolution,[status(thm)],[c62,clause13]) ).
cnf(c483,plain,
( skc8 != X749
| skc14 != X750
| general(X749,X750) ),
inference(resolution,[status(thm)],[c13,c70]) ).
cnf(c736,plain,
( skc8 != X751
| general(X751,skc14) ),
inference(resolution,[status(thm)],[c483,reflexivity]) ).
cnf(c59,plain,
relation(skc8,skc11),
inference(resolution,[status(thm)],[clause16,c57]) ).
cnf(c61,plain,
abstraction(skc8,skc11),
inference(resolution,[status(thm)],[c59,clause10]) ).
cnf(c66,plain,
general(skc8,skc11),
inference(resolution,[status(thm)],[c61,clause13]) ).
cnf(c482,plain,
( skc8 != X746
| skc11 != X747
| general(X746,X747) ),
inference(resolution,[status(thm)],[c13,c66]) ).
cnf(c734,plain,
( skc8 != X748
| general(X748,skc11) ),
inference(resolution,[status(thm)],[c482,reflexivity]) ).
cnf(clause49,axiom,
( ~ accessible_world(X139,X138)
| ~ relation(X139,X137)
| relation(X138,X137) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause49) ).
cnf(c201,plain,
( ~ accessible_world(skc8,X211)
| relation(X211,skc14) ),
inference(resolution,[status(thm)],[clause49,c60]) ).
cnf(c281,plain,
relation(skc10,skc14),
inference(resolution,[status(thm)],[c201,clause83]) ).
cnf(c282,plain,
abstraction(skc10,skc14),
inference(resolution,[status(thm)],[c281,clause10]) ).
cnf(c290,plain,
general(skc10,skc14),
inference(resolution,[status(thm)],[c282,clause13]) ).
cnf(c481,plain,
( skc10 != X743
| skc14 != X744
| general(X743,X744) ),
inference(resolution,[status(thm)],[c13,c290]) ).
cnf(c732,plain,
( skc10 != X745
| general(X745,skc14) ),
inference(resolution,[status(thm)],[c481,reflexivity]) ).
cnf(c200,plain,
( ~ accessible_world(skc8,X207)
| relation(X207,skc11) ),
inference(resolution,[status(thm)],[clause49,c59]) ).
cnf(c268,plain,
relation(skc10,skc11),
inference(resolution,[status(thm)],[c200,clause83]) ).
cnf(c269,plain,
abstraction(skc10,skc11),
inference(resolution,[status(thm)],[c268,clause10]) ).
cnf(c275,plain,
general(skc10,skc11),
inference(resolution,[status(thm)],[c269,clause13]) ).
cnf(c480,plain,
( skc10 != X740
| skc11 != X741
| general(X740,X741) ),
inference(resolution,[status(thm)],[c13,c275]) ).
cnf(c730,plain,
( skc10 != X742
| general(X742,skc11) ),
inference(resolution,[status(thm)],[c480,reflexivity]) ).
cnf(clause48,axiom,
( ~ accessible_world(X134,X133)
| ~ proposition(X134,X132)
| proposition(X133,X132) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause48) ).
cnf(c196,plain,
( ~ accessible_world(skc8,X196)
| proposition(X196,skc10) ),
inference(resolution,[status(thm)],[clause48,clause82]) ).
cnf(c248,plain,
proposition(skc10,skc10),
inference(resolution,[status(thm)],[c196,clause83]) ).
cnf(c252,plain,
relation(skc10,skc10),
inference(resolution,[status(thm)],[c248,clause9]) ).
cnf(c253,plain,
abstraction(skc10,skc10),
inference(resolution,[status(thm)],[c252,clause10]) ).
cnf(c259,plain,
general(skc10,skc10),
inference(resolution,[status(thm)],[c253,clause13]) ).
cnf(c479,plain,
( skc10 != X735
| skc10 != X736
| general(X735,X736) ),
inference(resolution,[status(thm)],[c13,c259]) ).
cnf(c726,plain,
( skc10 != X739
| general(X739,skc10) ),
inference(resolution,[status(thm)],[c479,reflexivity]) ).
cnf(clause12,axiom,
( ~ abstraction(X26,X25)
| nonhuman(X26,X25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
cnf(c65,plain,
nonhuman(skc8,skc11),
inference(resolution,[status(thm)],[c61,clause12]) ).
cnf(c12,axiom,
( X362 != X365
| X364 != X363
| ~ nonhuman(X362,X364)
| nonhuman(X365,X363) ),
theory(equality) ).
cnf(c477,plain,
( skc8 != X733
| skc11 != X734
| nonhuman(X733,X734) ),
inference(resolution,[status(thm)],[c12,c65]) ).
cnf(c724,plain,
( skc8 != X738
| nonhuman(X738,skc11) ),
inference(resolution,[status(thm)],[c477,reflexivity]) ).
cnf(c725,plain,
( skc10 != X737
| general(X737,X737) ),
inference(factor,[status(thm)],[c479]) ).
cnf(c69,plain,
nonhuman(skc8,skc14),
inference(resolution,[status(thm)],[c62,clause12]) ).
cnf(c476,plain,
( skc8 != X729
| skc14 != X730
| nonhuman(X729,X730) ),
inference(resolution,[status(thm)],[c12,c69]) ).
cnf(c721,plain,
( skc8 != X732
| nonhuman(X732,skc14) ),
inference(resolution,[status(thm)],[c476,reflexivity]) ).
cnf(c287,plain,
nonhuman(skc10,skc14),
inference(resolution,[status(thm)],[c282,clause12]) ).
cnf(c475,plain,
( skc10 != X727
| skc14 != X728
| nonhuman(X727,X728) ),
inference(resolution,[status(thm)],[c12,c287]) ).
cnf(c720,plain,
( skc10 != X731
| nonhuman(X731,skc14) ),
inference(resolution,[status(thm)],[c475,reflexivity]) ).
cnf(c256,plain,
nonhuman(skc10,skc10),
inference(resolution,[status(thm)],[c253,clause12]) ).
cnf(c474,plain,
( skc10 != X723
| skc10 != X724
| nonhuman(X723,X724) ),
inference(resolution,[status(thm)],[c12,c256]) ).
cnf(c717,plain,
( skc10 != X726
| nonhuman(X726,skc10) ),
inference(resolution,[status(thm)],[c474,reflexivity]) ).
cnf(c716,plain,
( skc10 != X725
| nonhuman(X725,X725) ),
inference(factor,[status(thm)],[c474]) ).
cnf(c272,plain,
nonhuman(skc10,skc11),
inference(resolution,[status(thm)],[c269,clause12]) ).
cnf(c473,plain,
( skc10 != X720
| skc11 != X721
| nonhuman(X720,X721) ),
inference(resolution,[status(thm)],[c12,c272]) ).
cnf(c714,plain,
( skc10 != X722
| nonhuman(X722,skc11) ),
inference(resolution,[status(thm)],[c473,reflexivity]) ).
cnf(c54,plain,
nonhuman(skc8,skc10),
inference(resolution,[status(thm)],[clause12,c51]) ).
cnf(c472,plain,
( skc8 != X717
| skc10 != X718
| nonhuman(X717,X718) ),
inference(resolution,[status(thm)],[c12,c54]) ).
cnf(c712,plain,
( skc8 != X719
| nonhuman(X719,skc10) ),
inference(resolution,[status(thm)],[c472,reflexivity]) ).
cnf(c11,axiom,
( X357 != X360
| X359 != X358
| ~ abstraction(X357,X359)
| abstraction(X360,X358) ),
theory(equality) ).
cnf(c463,plain,
( skc8 != X714
| skc10 != X715
| abstraction(X714,X715) ),
inference(resolution,[status(thm)],[c11,c51]) ).
cnf(c710,plain,
( skc8 != X716
| abstraction(X716,skc10) ),
inference(resolution,[status(thm)],[c463,reflexivity]) ).
cnf(c462,plain,
( skc8 != X711
| skc14 != X712
| abstraction(X711,X712) ),
inference(resolution,[status(thm)],[c11,c62]) ).
cnf(c708,plain,
( skc8 != X713
| abstraction(X713,skc14) ),
inference(resolution,[status(thm)],[c462,reflexivity]) ).
cnf(c461,plain,
( skc10 != X708
| skc14 != X709
| abstraction(X708,X709) ),
inference(resolution,[status(thm)],[c11,c282]) ).
cnf(c706,plain,
( skc10 != X710
| abstraction(X710,skc14) ),
inference(resolution,[status(thm)],[c461,reflexivity]) ).
cnf(c460,plain,
( skc8 != X705
| skc11 != X706
| abstraction(X705,X706) ),
inference(resolution,[status(thm)],[c11,c61]) ).
cnf(c704,plain,
( skc8 != X707
| abstraction(X707,skc11) ),
inference(resolution,[status(thm)],[c460,reflexivity]) ).
cnf(c459,plain,
( skc10 != X701
| skc11 != X702
| abstraction(X701,X702) ),
inference(resolution,[status(thm)],[c11,c269]) ).
cnf(c701,plain,
( skc10 != X704
| abstraction(X704,skc11) ),
inference(resolution,[status(thm)],[c459,reflexivity]) ).
cnf(c458,plain,
( skc10 != X696
| skc10 != X697
| abstraction(X696,X697) ),
inference(resolution,[status(thm)],[c11,c253]) ).
cnf(c697,plain,
( skc10 != X703
| abstraction(X703,skc10) ),
inference(resolution,[status(thm)],[c458,reflexivity]) ).
cnf(c10,axiom,
( X350 != X353
| X352 != X351
| ~ relation(X350,X352)
| relation(X353,X351) ),
theory(equality) ).
cnf(c454,plain,
( skc10 != X695
| skc10 != X694
| relation(X695,X694) ),
inference(resolution,[status(thm)],[c10,c252]) ).
cnf(c695,plain,
( skc10 != X700
| relation(X700,skc10) ),
inference(resolution,[status(thm)],[c454,reflexivity]) ).
cnf(c696,plain,
( skc10 != X699
| abstraction(X699,X699) ),
inference(factor,[status(thm)],[c458]) ).
cnf(c694,plain,
( skc10 != X698
| relation(X698,X698) ),
inference(factor,[status(thm)],[c454]) ).
cnf(c453,plain,
( skc8 != X691
| skc14 != X690
| relation(X691,X690) ),
inference(resolution,[status(thm)],[c10,c60]) ).
cnf(c691,plain,
( skc8 != X693
| relation(X693,skc14) ),
inference(resolution,[status(thm)],[c453,reflexivity]) ).
cnf(c452,plain,
( skc10 != X689
| skc14 != X688
| relation(X689,X688) ),
inference(resolution,[status(thm)],[c10,c281]) ).
cnf(c690,plain,
( skc10 != X692
| relation(X692,skc14) ),
inference(resolution,[status(thm)],[c452,reflexivity]) ).
cnf(c451,plain,
( skc10 != X685
| skc11 != X684
| relation(X685,X684) ),
inference(resolution,[status(thm)],[c10,c268]) ).
cnf(c687,plain,
( skc10 != X687
| relation(X687,skc11) ),
inference(resolution,[status(thm)],[c451,reflexivity]) ).
cnf(c450,plain,
( skc8 != X683
| skc11 != X682
| relation(X683,X682) ),
inference(resolution,[status(thm)],[c10,c59]) ).
cnf(c686,plain,
( skc8 != X686
| relation(X686,skc11) ),
inference(resolution,[status(thm)],[c450,reflexivity]) ).
cnf(c449,plain,
( skc8 != X679
| skc10 != X678
| relation(X679,X678) ),
inference(resolution,[status(thm)],[c10,c50]) ).
cnf(c683,plain,
( skc8 != X681
| relation(X681,skc10) ),
inference(resolution,[status(thm)],[c449,reflexivity]) ).
cnf(c9,axiom,
( X342 != X345
| X344 != X343
| ~ proposition(X342,X344)
| proposition(X345,X343) ),
theory(equality) ).
cnf(c447,plain,
( skc8 != X676
| skc10 != X677
| proposition(X676,X677) ),
inference(resolution,[status(thm)],[c9,clause82]) ).
cnf(c682,plain,
( skc8 != X680
| proposition(X680,skc10) ),
inference(resolution,[status(thm)],[c447,reflexivity]) ).
cnf(c446,plain,
( skc10 != X672
| skc10 != X673
| proposition(X672,X673) ),
inference(resolution,[status(thm)],[c9,c248]) ).
cnf(c679,plain,
( skc10 != X675
| proposition(X675,skc10) ),
inference(resolution,[status(thm)],[c446,reflexivity]) ).
cnf(c678,plain,
( skc10 != X674
| proposition(X674,X674) ),
inference(factor,[status(thm)],[c446]) ).
cnf(clause84,negated_conjecture,
desire_want(skc8,skc9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause84) ).
cnf(clause47,axiom,
( ~ accessible_world(X128,X127)
| ~ desire_want(X128,X126)
| desire_want(X127,X126) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause47) ).
cnf(c192,plain,
( ~ accessible_world(skc8,X195)
| desire_want(X195,skc9) ),
inference(resolution,[status(thm)],[clause47,clause84]) ).
cnf(c245,plain,
desire_want(skc10,skc9),
inference(resolution,[status(thm)],[c192,clause83]) ).
cnf(c8,axiom,
( X335 != X338
| X337 != X336
| ~ desire_want(X335,X337)
| desire_want(X338,X336) ),
theory(equality) ).
cnf(c443,plain,
( skc10 != X669
| skc9 != X670
| desire_want(X669,X670) ),
inference(resolution,[status(thm)],[c8,c245]) ).
cnf(c676,plain,
( skc10 != X671
| desire_want(X671,skc9) ),
inference(resolution,[status(thm)],[c443,reflexivity]) ).
cnf(c442,plain,
( skc8 != X666
| skc9 != X667
| desire_want(X666,X667) ),
inference(resolution,[status(thm)],[c8,clause84]) ).
cnf(c674,plain,
( skc8 != X668
| desire_want(X668,skc9) ),
inference(resolution,[status(thm)],[c442,reflexivity]) ).
cnf(clause14,axiom,
( ~ abstraction(X30,X29)
| unisex(X30,X29) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
cnf(c64,plain,
unisex(skc8,skc11),
inference(resolution,[status(thm)],[c61,clause14]) ).
cnf(c7,axiom,
( X328 != X331
| X330 != X329
| ~ unisex(X328,X330)
| unisex(X331,X329) ),
theory(equality) ).
cnf(c439,plain,
( skc8 != X663
| skc11 != X664
| unisex(X663,X664) ),
inference(resolution,[status(thm)],[c7,c64]) ).
cnf(c672,plain,
( skc8 != X665
| unisex(X665,skc11) ),
inference(resolution,[status(thm)],[c439,reflexivity]) ).
cnf(clause76,negated_conjecture,
event(skc10,skc13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause76) ).
cnf(clause2,axiom,
( ~ event(X6,X5)
| eventuality(X6,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
cnf(c37,plain,
eventuality(skc10,skc13),
inference(resolution,[status(thm)],[clause2,clause76]) ).
cnf(clause7,axiom,
( ~ eventuality(X16,X15)
| unisex(X16,X15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
cnf(c42,plain,
unisex(skc10,skc13),
inference(resolution,[status(thm)],[clause7,c37]) ).
cnf(c438,plain,
( skc10 != X660
| skc13 != X661
| unisex(X660,X661) ),
inference(resolution,[status(thm)],[c7,c42]) ).
cnf(c670,plain,
( skc10 != X662
| unisex(X662,skc13) ),
inference(resolution,[status(thm)],[c438,reflexivity]) ).
cnf(c56,plain,
unisex(skc8,skc10),
inference(resolution,[status(thm)],[clause14,c51]) ).
cnf(c437,plain,
( skc8 != X657
| skc10 != X658
| unisex(X657,X658) ),
inference(resolution,[status(thm)],[c7,c56]) ).
cnf(c668,plain,
( skc8 != X659
| unisex(X659,skc10) ),
inference(resolution,[status(thm)],[c437,reflexivity]) ).
cnf(clause8,axiom,
( ~ desire_want(X18,X17)
| event(X18,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
cnf(c43,plain,
event(skc8,skc9),
inference(resolution,[status(thm)],[clause8,clause84]) ).
cnf(clause39,axiom,
( ~ accessible_world(X85,X84)
| ~ event(X85,X83)
| event(X84,X83) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause39) ).
cnf(c122,plain,
( ~ accessible_world(skc8,X91)
| event(X91,skc9) ),
inference(resolution,[status(thm)],[clause39,c43]) ).
cnf(c124,plain,
event(skc10,skc9),
inference(resolution,[status(thm)],[c122,clause83]) ).
cnf(c128,plain,
eventuality(skc10,skc9),
inference(resolution,[status(thm)],[c124,clause2]) ).
cnf(c131,plain,
unisex(skc10,skc9),
inference(resolution,[status(thm)],[c128,clause7]) ).
cnf(c436,plain,
( skc10 != X654
| skc9 != X655
| unisex(X654,X655) ),
inference(resolution,[status(thm)],[c7,c131]) ).
cnf(c666,plain,
( skc10 != X656
| unisex(X656,skc9) ),
inference(resolution,[status(thm)],[c436,reflexivity]) ).
cnf(c44,plain,
eventuality(skc8,skc9),
inference(resolution,[status(thm)],[c43,clause2]) ).
cnf(c48,plain,
unisex(skc8,skc9),
inference(resolution,[status(thm)],[c44,clause7]) ).
cnf(c435,plain,
( skc8 != X651
| skc9 != X652
| unisex(X651,X652) ),
inference(resolution,[status(thm)],[c7,c48]) ).
cnf(c664,plain,
( skc8 != X653
| unisex(X653,skc9) ),
inference(resolution,[status(thm)],[c435,reflexivity]) ).
cnf(c68,plain,
unisex(skc8,skc14),
inference(resolution,[status(thm)],[c62,clause14]) ).
cnf(c434,plain,
( skc8 != X648
| skc14 != X649
| unisex(X648,X649) ),
inference(resolution,[status(thm)],[c7,c68]) ).
cnf(c662,plain,
( skc8 != X650
| unisex(X650,skc14) ),
inference(resolution,[status(thm)],[c434,reflexivity]) ).
cnf(clause45,axiom,
( ~ accessible_world(X117,X116)
| ~ unisex(X117,X115)
| unisex(X116,X115) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause45) ).
cnf(c178,plain,
( ~ accessible_world(skc8,X173)
| unisex(X173,skc10) ),
inference(resolution,[status(thm)],[clause45,c56]) ).
cnf(c229,plain,
unisex(skc10,skc10),
inference(resolution,[status(thm)],[c178,clause83]) ).
cnf(c433,plain,
( skc10 != X644
| skc10 != X645
| unisex(X644,X645) ),
inference(resolution,[status(thm)],[c7,c229]) ).
cnf(c659,plain,
( skc10 != X647
| unisex(X647,skc10) ),
inference(resolution,[status(thm)],[c433,reflexivity]) ).
cnf(c658,plain,
( skc10 != X646
| unisex(X646,X646) ),
inference(factor,[status(thm)],[c433]) ).
cnf(c180,plain,
( ~ accessible_world(skc8,X178)
| unisex(X178,skc11) ),
inference(resolution,[status(thm)],[clause45,c64]) ).
cnf(c234,plain,
unisex(skc10,skc11),
inference(resolution,[status(thm)],[c180,clause83]) ).
cnf(c432,plain,
( skc10 != X641
| skc11 != X642
| unisex(X641,X642) ),
inference(resolution,[status(thm)],[c7,c234]) ).
cnf(c656,plain,
( skc10 != X643
| unisex(X643,skc11) ),
inference(resolution,[status(thm)],[c432,reflexivity]) ).
cnf(c175,plain,
( ~ accessible_world(skc8,X167)
| unisex(X167,skc14) ),
inference(resolution,[status(thm)],[clause45,c68]) ).
cnf(c222,plain,
unisex(skc10,skc14),
inference(resolution,[status(thm)],[c175,clause83]) ).
cnf(c431,plain,
( skc10 != X638
| skc14 != X639
| unisex(X638,X639) ),
inference(resolution,[status(thm)],[c7,c222]) ).
cnf(c654,plain,
( skc10 != X640
| unisex(X640,skc14) ),
inference(resolution,[status(thm)],[c431,reflexivity]) ).
cnf(clause6,axiom,
( ~ eventuality(X14,X13)
| nonexistent(X14,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
cnf(c41,plain,
nonexistent(skc10,skc13),
inference(resolution,[status(thm)],[clause6,c37]) ).
cnf(c6,axiom,
( X320 != X323
| X322 != X321
| ~ nonexistent(X320,X322)
| nonexistent(X323,X321) ),
theory(equality) ).
cnf(c429,plain,
( skc10 != X636
| skc13 != X635
| nonexistent(X636,X635) ),
inference(resolution,[status(thm)],[c6,c41]) ).
cnf(c652,plain,
( skc10 != X637
| nonexistent(X637,skc13) ),
inference(resolution,[status(thm)],[c429,reflexivity]) ).
cnf(c45,plain,
nonexistent(skc8,skc9),
inference(resolution,[status(thm)],[c44,clause6]) ).
cnf(c428,plain,
( skc8 != X633
| skc9 != X632
| nonexistent(X633,X632) ),
inference(resolution,[status(thm)],[c6,c45]) ).
cnf(c650,plain,
( skc8 != X634
| nonexistent(X634,skc9) ),
inference(resolution,[status(thm)],[c428,reflexivity]) ).
cnf(c132,plain,
nonexistent(skc10,skc9),
inference(resolution,[status(thm)],[c128,clause6]) ).
cnf(c427,plain,
( skc10 != X630
| skc9 != X629
| nonexistent(X630,X629) ),
inference(resolution,[status(thm)],[c6,c132]) ).
cnf(c648,plain,
( skc10 != X631
| nonexistent(X631,skc9) ),
inference(resolution,[status(thm)],[c427,reflexivity]) ).
cnf(clause22,axiom,
( ~ entity(X46,X45)
| specific(X46,X45) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
cnf(c96,plain,
specific(skc8,skc15),
inference(resolution,[status(thm)],[c92,clause22]) ).
cnf(clause43,axiom,
( ~ accessible_world(X107,X106)
| ~ specific(X107,X105)
| specific(X106,X105) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause43) ).
cnf(c157,plain,
( ~ accessible_world(skc8,X147)
| specific(X147,skc15) ),
inference(resolution,[status(thm)],[clause43,c96]) ).
cnf(c209,plain,
specific(skc10,skc15),
inference(resolution,[status(thm)],[c157,clause83]) ).
cnf(c5,axiom,
( X313 != X316
| X315 != X314
| ~ specific(X313,X315)
| specific(X316,X314) ),
theory(equality) ).
cnf(c424,plain,
( skc10 != X626
| skc15 != X627
| specific(X626,X627) ),
inference(resolution,[status(thm)],[c5,c209]) ).
cnf(c646,plain,
( skc10 != X628
| specific(X628,skc15) ),
inference(resolution,[status(thm)],[c424,reflexivity]) ).
cnf(c78,plain,
specific(skc8,skc12),
inference(resolution,[status(thm)],[clause22,c76]) ).
cnf(c156,plain,
( ~ accessible_world(skc8,X143)
| specific(X143,skc12) ),
inference(resolution,[status(thm)],[clause43,c78]) ).
cnf(c203,plain,
specific(skc10,skc12),
inference(resolution,[status(thm)],[c156,clause83]) ).
cnf(c423,plain,
( skc10 != X623
| skc12 != X624
| specific(X623,X624) ),
inference(resolution,[status(thm)],[c5,c203]) ).
cnf(c644,plain,
( skc10 != X625
| specific(X625,skc12) ),
inference(resolution,[status(thm)],[c423,reflexivity]) ).
cnf(clause5,axiom,
( ~ eventuality(X12,X11)
| specific(X12,X11) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
cnf(c46,plain,
specific(skc8,skc9),
inference(resolution,[status(thm)],[c44,clause5]) ).
cnf(c422,plain,
( skc8 != X620
| skc9 != X621
| specific(X620,X621) ),
inference(resolution,[status(thm)],[c5,c46]) ).
cnf(c642,plain,
( skc8 != X622
| specific(X622,skc9) ),
inference(resolution,[status(thm)],[c422,reflexivity]) ).
cnf(c40,plain,
specific(skc10,skc13),
inference(resolution,[status(thm)],[clause5,c37]) ).
cnf(c421,plain,
( skc10 != X617
| skc13 != X618
| specific(X617,X618) ),
inference(resolution,[status(thm)],[c5,c40]) ).
cnf(c640,plain,
( skc10 != X619
| specific(X619,skc13) ),
inference(resolution,[status(thm)],[c421,reflexivity]) ).
cnf(c420,plain,
( skc8 != X614
| skc15 != X615
| specific(X614,X615) ),
inference(resolution,[status(thm)],[c5,c96]) ).
cnf(c638,plain,
( skc8 != X616
| specific(X616,skc15) ),
inference(resolution,[status(thm)],[c420,reflexivity]) ).
cnf(c419,plain,
( skc8 != X611
| skc12 != X612
| specific(X611,X612) ),
inference(resolution,[status(thm)],[c5,c78]) ).
cnf(c636,plain,
( skc8 != X613
| specific(X613,skc12) ),
inference(resolution,[status(thm)],[c419,reflexivity]) ).
cnf(c133,plain,
specific(skc10,skc9),
inference(resolution,[status(thm)],[c128,clause5]) ).
cnf(c418,plain,
( skc10 != X608
| skc9 != X609
| specific(X608,X609) ),
inference(resolution,[status(thm)],[c5,c133]) ).
cnf(c634,plain,
( skc10 != X610
| specific(X610,skc9) ),
inference(resolution,[status(thm)],[c418,reflexivity]) ).
cnf(clause4,axiom,
( ~ thing(X10,X9)
| singleton(X10,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
cnf(clause11,axiom,
( ~ abstraction(X24,X23)
| thing(X24,X23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(c67,plain,
thing(skc8,skc14),
inference(resolution,[status(thm)],[c62,clause11]) ).
cnf(clause41,axiom,
( ~ accessible_world(X97,X96)
| ~ thing(X97,X95)
| thing(X96,X95) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause41) ).
cnf(c143,plain,
( ~ accessible_world(skc8,X123)
| thing(X123,skc14) ),
inference(resolution,[status(thm)],[clause41,c67]) ).
cnf(c188,plain,
thing(skc10,skc14),
inference(resolution,[status(thm)],[c143,clause83]) ).
cnf(c190,plain,
singleton(skc10,skc14),
inference(resolution,[status(thm)],[c188,clause4]) ).
cnf(c4,axiom,
( X305 != X308
| X307 != X306
| ~ singleton(X305,X307)
| singleton(X308,X306) ),
theory(equality) ).
cnf(c416,plain,
( skc10 != X606
| skc14 != X605
| singleton(X606,X605) ),
inference(resolution,[status(thm)],[c4,c190]) ).
cnf(c632,plain,
( skc10 != X607
| singleton(X607,skc14) ),
inference(resolution,[status(thm)],[c416,reflexivity]) ).
cnf(clause3,axiom,
( ~ eventuality(X8,X7)
| thing(X8,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(c38,plain,
thing(skc10,skc13),
inference(resolution,[status(thm)],[c37,clause3]) ).
cnf(c39,plain,
singleton(skc10,skc13),
inference(resolution,[status(thm)],[clause4,c38]) ).
cnf(c415,plain,
( skc10 != X603
| skc13 != X602
| singleton(X603,X602) ),
inference(resolution,[status(thm)],[c4,c39]) ).
cnf(c630,plain,
( skc10 != X604
| singleton(X604,skc13) ),
inference(resolution,[status(thm)],[c415,reflexivity]) ).
cnf(clause93,negated_conjecture,
( ~ present(skc8,X272)
| ~ desire_want(skc8,X272)
| ~ agent(skc8,X272,skc15)
| ~ dance(X271,X270)
| ~ present(X271,X270)
| ~ agent(X271,X270,skc15)
| ~ event(X271,X270)
| ~ accessible_world(skc8,X271)
| ~ theme(skc8,X272,X271)
| ~ proposition(skc8,X271) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause93) ).
cnf(c355,plain,
( ~ present(skc8,skc9)
| ~ desire_want(skc8,skc9)
| ~ agent(skc8,skc9,skc15)
| ~ dance(skc10,X601)
| ~ present(skc10,X601)
| ~ agent(skc10,X601,skc15)
| ~ event(skc10,X601)
| ~ accessible_world(skc8,skc10)
| ~ proposition(skc8,skc10) ),
inference(resolution,[status(thm)],[clause93,clause92]) ).
cnf(c52,plain,
thing(skc8,skc10),
inference(resolution,[status(thm)],[clause11,c51]) ).
cnf(c140,plain,
( ~ accessible_world(skc8,X114)
| thing(X114,skc10) ),
inference(resolution,[status(thm)],[clause41,c52]) ).
cnf(c172,plain,
thing(skc10,skc10),
inference(resolution,[status(thm)],[c140,clause83]) ).
cnf(c174,plain,
singleton(skc10,skc10),
inference(resolution,[status(thm)],[c172,clause4]) ).
cnf(c414,plain,
( skc10 != X598
| skc10 != X597
| singleton(X598,X597) ),
inference(resolution,[status(thm)],[c4,c174]) ).
cnf(c627,plain,
( skc10 != X600
| singleton(X600,skc10) ),
inference(resolution,[status(thm)],[c414,reflexivity]) ).
cnf(c626,plain,
( skc10 != X599
| singleton(X599,X599) ),
inference(factor,[status(thm)],[c414]) ).
cnf(c348,plain,
( ~ theme(skc8,X596,X595)
| ~ desire_want(skc8,X596)
| ~ proposition(skc8,X595)
| ~ proposition(skc8,skc10)
| ~ desire_want(skc8,skc9)
| skc10 = X595 ),
inference(resolution,[status(thm)],[clause73,clause92]) ).
cnf(clause21,axiom,
( ~ entity(X44,X43)
| thing(X44,X43) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
cnf(c77,plain,
thing(skc8,skc12),
inference(resolution,[status(thm)],[clause21,c76]) ).
cnf(c142,plain,
( ~ accessible_world(skc8,X119)
| thing(X119,skc12) ),
inference(resolution,[status(thm)],[clause41,c77]) ).
cnf(c182,plain,
thing(skc10,skc12),
inference(resolution,[status(thm)],[c142,clause83]) ).
cnf(c184,plain,
singleton(skc10,skc12),
inference(resolution,[status(thm)],[c182,clause4]) ).
cnf(c413,plain,
( skc10 != X593
| skc12 != X592
| singleton(X593,X592) ),
inference(resolution,[status(thm)],[c4,c184]) ).
cnf(c623,plain,
( skc10 != X594
| singleton(X594,skc12) ),
inference(resolution,[status(thm)],[c413,reflexivity]) ).
cnf(c95,plain,
thing(skc8,skc15),
inference(resolution,[status(thm)],[c92,clause21]) ).
cnf(c139,plain,
( ~ accessible_world(skc8,X113)
| thing(X113,skc15) ),
inference(resolution,[status(thm)],[clause41,c95]) ).
cnf(c168,plain,
thing(skc10,skc15),
inference(resolution,[status(thm)],[c139,clause83]) ).
cnf(c170,plain,
singleton(skc10,skc15),
inference(resolution,[status(thm)],[c168,clause4]) ).
cnf(c412,plain,
( skc10 != X587
| skc15 != X586
| singleton(X587,X586) ),
inference(resolution,[status(thm)],[c4,c170]) ).
cnf(c621,plain,
( skc10 != X591
| singleton(X591,skc15) ),
inference(resolution,[status(thm)],[c412,reflexivity]) ).
cnf(c98,plain,
singleton(skc8,skc15),
inference(resolution,[status(thm)],[c95,clause4]) ).
cnf(c411,plain,
( skc8 != X584
| skc15 != X583
| singleton(X584,X583) ),
inference(resolution,[status(thm)],[c4,c98]) ).
cnf(c619,plain,
( skc8 != X585
| singleton(X585,skc15) ),
inference(resolution,[status(thm)],[c411,reflexivity]) ).
cnf(c335,plain,
( ~ forename(skc8,skc14)
| ~ of(skc8,X582,skc15)
| ~ forename(skc8,X582)
| ~ entity(skc8,skc15)
| X582 = skc14 ),
inference(resolution,[status(thm)],[clause72,clause88]) ).
cnf(c63,plain,
thing(skc8,skc11),
inference(resolution,[status(thm)],[c61,clause11]) ).
cnf(c71,plain,
singleton(skc8,skc11),
inference(resolution,[status(thm)],[c63,clause4]) ).
cnf(c410,plain,
( skc8 != X580
| skc11 != X579
| singleton(X580,X579) ),
inference(resolution,[status(thm)],[c4,c71]) ).
cnf(c616,plain,
( skc8 != X581
| singleton(X581,skc11) ),
inference(resolution,[status(thm)],[c410,reflexivity]) ).
cnf(c73,plain,
singleton(skc8,skc14),
inference(resolution,[status(thm)],[c67,clause4]) ).
cnf(c409,plain,
( skc8 != X577
| skc14 != X576
| singleton(X577,X576) ),
inference(resolution,[status(thm)],[c4,c73]) ).
cnf(c614,plain,
( skc8 != X578
| singleton(X578,skc14) ),
inference(resolution,[status(thm)],[c409,reflexivity]) ).
cnf(c334,plain,
( ~ forename(skc8,skc11)
| ~ of(skc8,X575,skc12)
| ~ forename(skc8,X575)
| ~ entity(skc8,skc12)
| X575 = skc11 ),
inference(resolution,[status(thm)],[clause72,clause89]) ).
cnf(c137,plain,
( ~ accessible_world(skc8,X108)
| thing(X108,skc11) ),
inference(resolution,[status(thm)],[clause41,c63]) ).
cnf(c160,plain,
thing(skc10,skc11),
inference(resolution,[status(thm)],[c137,clause83]) ).
cnf(c162,plain,
singleton(skc10,skc11),
inference(resolution,[status(thm)],[c160,clause4]) ).
cnf(c408,plain,
( skc10 != X573
| skc11 != X572
| singleton(X573,X572) ),
inference(resolution,[status(thm)],[c4,c162]) ).
cnf(c611,plain,
( skc10 != X574
| singleton(X574,skc11) ),
inference(resolution,[status(thm)],[c408,reflexivity]) ).
cnf(c79,plain,
singleton(skc8,skc12),
inference(resolution,[status(thm)],[c77,clause4]) ).
cnf(c407,plain,
( skc8 != X567
| skc12 != X566
| singleton(X567,X566) ),
inference(resolution,[status(thm)],[c4,c79]) ).
cnf(c609,plain,
( skc8 != X571
| singleton(X571,skc12) ),
inference(resolution,[status(thm)],[c407,reflexivity]) ).
cnf(c53,plain,
singleton(skc8,skc10),
inference(resolution,[status(thm)],[c52,clause4]) ).
cnf(c406,plain,
( skc8 != X564
| skc10 != X563
| singleton(X564,X563) ),
inference(resolution,[status(thm)],[c4,c53]) ).
cnf(c607,plain,
( skc8 != X565
| singleton(X565,skc10) ),
inference(resolution,[status(thm)],[c406,reflexivity]) ).
cnf(c47,plain,
thing(skc8,skc9),
inference(resolution,[status(thm)],[c44,clause3]) ).
cnf(c49,plain,
singleton(skc8,skc9),
inference(resolution,[status(thm)],[c47,clause4]) ).
cnf(c405,plain,
( skc8 != X555
| skc9 != X554
| singleton(X555,X554) ),
inference(resolution,[status(thm)],[c4,c49]) ).
cnf(c601,plain,
( skc8 != X556
| singleton(X556,skc9) ),
inference(resolution,[status(thm)],[c405,reflexivity]) ).
cnf(c130,plain,
thing(skc10,skc9),
inference(resolution,[status(thm)],[c128,clause3]) ).
cnf(c134,plain,
singleton(skc10,skc9),
inference(resolution,[status(thm)],[c130,clause4]) ).
cnf(c404,plain,
( skc10 != X552
| skc9 != X551
| singleton(X552,X551) ),
inference(resolution,[status(thm)],[c4,c134]) ).
cnf(c599,plain,
( skc10 != X553
| singleton(X553,skc9) ),
inference(resolution,[status(thm)],[c404,reflexivity]) ).
cnf(c3,axiom,
( X298 != X301
| X300 != X299
| ~ thing(X298,X300)
| thing(X301,X299) ),
theory(equality) ).
cnf(c401,plain,
( skc10 != X543
| skc9 != X542
| thing(X543,X542) ),
inference(resolution,[status(thm)],[c3,c130]) ).
cnf(c595,plain,
( skc10 != X544
| thing(X544,skc9) ),
inference(resolution,[status(thm)],[c401,reflexivity]) ).
cnf(c400,plain,
( skc10 != X534
| skc14 != X533
| thing(X534,X533) ),
inference(resolution,[status(thm)],[c3,c188]) ).
cnf(c590,plain,
( skc10 != X541
| thing(X541,skc14) ),
inference(resolution,[status(thm)],[c400,reflexivity]) ).
cnf(c399,plain,
( skc10 != X531
| skc11 != X530
| thing(X531,X530) ),
inference(resolution,[status(thm)],[c3,c160]) ).
cnf(c588,plain,
( skc10 != X532
| thing(X532,skc11) ),
inference(resolution,[status(thm)],[c399,reflexivity]) ).
cnf(c398,plain,
( skc8 != X524
| skc14 != X523
| thing(X524,X523) ),
inference(resolution,[status(thm)],[c3,c67]) ).
cnf(c583,plain,
( skc8 != X525
| thing(X525,skc14) ),
inference(resolution,[status(thm)],[c398,reflexivity]) ).
cnf(c397,plain,
( skc8 != X521
| skc12 != X520
| thing(X521,X520) ),
inference(resolution,[status(thm)],[c3,c77]) ).
cnf(c581,plain,
( skc8 != X522
| thing(X522,skc12) ),
inference(resolution,[status(thm)],[c397,reflexivity]) ).
cnf(c396,plain,
( skc10 != X514
| skc13 != X513
| thing(X514,X513) ),
inference(resolution,[status(thm)],[c3,c38]) ).
cnf(c578,plain,
( skc10 != X515
| thing(X515,skc13) ),
inference(resolution,[status(thm)],[c396,reflexivity]) ).
cnf(c395,plain,
( skc8 != X507
| skc10 != X506
| thing(X507,X506) ),
inference(resolution,[status(thm)],[c3,c52]) ).
cnf(c574,plain,
( skc8 != X512
| thing(X512,skc10) ),
inference(resolution,[status(thm)],[c395,reflexivity]) ).
cnf(c394,plain,
( skc10 != X499
| skc10 != X498
| thing(X499,X498) ),
inference(resolution,[status(thm)],[c3,c172]) ).
cnf(c569,plain,
( skc10 != X505
| thing(X505,skc10) ),
inference(resolution,[status(thm)],[c394,reflexivity]) ).
cnf(c568,plain,
( skc10 != X504
| thing(X504,X504) ),
inference(factor,[status(thm)],[c394]) ).
cnf(c393,plain,
( skc8 != X496
| skc15 != X495
| thing(X496,X495) ),
inference(resolution,[status(thm)],[c3,c95]) ).
cnf(c566,plain,
( skc8 != X497
| thing(X497,skc15) ),
inference(resolution,[status(thm)],[c393,reflexivity]) ).
cnf(c392,plain,
( skc8 != X489
| skc9 != X488
| thing(X489,X488) ),
inference(resolution,[status(thm)],[c3,c47]) ).
cnf(c562,plain,
( skc8 != X490
| thing(X490,skc9) ),
inference(resolution,[status(thm)],[c392,reflexivity]) ).
cnf(c391,plain,
( skc8 != X486
| skc11 != X485
| thing(X486,X485) ),
inference(resolution,[status(thm)],[c3,c63]) ).
cnf(c560,plain,
( skc8 != X487
| thing(X487,skc11) ),
inference(resolution,[status(thm)],[c391,reflexivity]) ).
cnf(c390,plain,
( skc10 != X479
| skc12 != X478
| thing(X479,X478) ),
inference(resolution,[status(thm)],[c3,c182]) ).
cnf(c556,plain,
( skc10 != X480
| thing(X480,skc12) ),
inference(resolution,[status(thm)],[c390,reflexivity]) ).
cnf(c389,plain,
( skc10 != X472
| skc15 != X471
| thing(X472,X471) ),
inference(resolution,[status(thm)],[c3,c168]) ).
cnf(c550,plain,
( skc10 != X477
| thing(X477,skc15) ),
inference(resolution,[status(thm)],[c389,reflexivity]) ).
cnf(c2,axiom,
( X291 != X294
| X293 != X292
| ~ eventuality(X291,X293)
| eventuality(X294,X292) ),
theory(equality) ).
cnf(c386,plain,
( skc10 != X468
| skc9 != X469
| eventuality(X468,X469) ),
inference(resolution,[status(thm)],[c2,c128]) ).
cnf(c548,plain,
( skc10 != X470
| eventuality(X470,skc9) ),
inference(resolution,[status(thm)],[c386,reflexivity]) ).
cnf(c385,plain,
( skc8 != X461
| skc9 != X462
| eventuality(X461,X462) ),
inference(resolution,[status(thm)],[c2,c44]) ).
cnf(c542,plain,
( skc8 != X463
| eventuality(X463,skc9) ),
inference(resolution,[status(thm)],[c385,reflexivity]) ).
cnf(c384,plain,
( skc10 != X458
| skc13 != X459
| eventuality(X458,X459) ),
inference(resolution,[status(thm)],[c2,c37]) ).
cnf(c540,plain,
( skc10 != X460
| eventuality(X460,skc13) ),
inference(resolution,[status(thm)],[c384,reflexivity]) ).
cnf(c1,axiom,
( X282 != X285
| X284 != X283
| ~ event(X282,X284)
| event(X285,X283) ),
theory(equality) ).
cnf(c382,plain,
( skc8 != X451
| skc9 != X452
| event(X451,X452) ),
inference(resolution,[status(thm)],[c1,c43]) ).
cnf(c534,plain,
( skc8 != X453
| event(X453,skc9) ),
inference(resolution,[status(thm)],[c382,reflexivity]) ).
cnf(c381,plain,
( skc10 != X444
| skc9 != X445
| event(X444,X445) ),
inference(resolution,[status(thm)],[c1,c124]) ).
cnf(c528,plain,
( skc10 != X450
| event(X450,skc9) ),
inference(resolution,[status(thm)],[c381,reflexivity]) ).
cnf(c380,plain,
( skc10 != X441
| skc13 != X442
| event(X441,X442) ),
inference(resolution,[status(thm)],[c1,clause76]) ).
cnf(c526,plain,
( skc10 != X443
| event(X443,skc13) ),
inference(resolution,[status(thm)],[c380,reflexivity]) ).
cnf(clause79,negated_conjecture,
dance(skc10,skc13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause79) ).
cnf(c0,axiom,
( X278 != X281
| X280 != X279
| ~ dance(X278,X280)
| dance(X281,X279) ),
theory(equality) ).
cnf(c376,plain,
( skc10 != X435
| skc13 != X434
| dance(X435,X434) ),
inference(resolution,[status(thm)],[c0,clause79]) ).
cnf(c520,plain,
( skc10 != X436
| dance(X436,skc13) ),
inference(resolution,[status(thm)],[c376,reflexivity]) ).
cnf(c514,plain,
( ~ accessible_world(skc10,X433)
| of(X433,skc14,skc15) ),
inference(resolution,[status(thm)],[c513,clause71]) ).
cnf(c511,plain,
( ~ accessible_world(skc10,X432)
| of(X432,skc11,skc12) ),
inference(resolution,[status(thm)],[c510,clause71]) ).
cnf(c505,plain,
( ~ accessible_world(skc10,X431)
| theme(X431,skc9,skc10) ),
inference(resolution,[status(thm)],[c503,clause70]) ).
cnf(c502,plain,
( ~ accessible_world(skc10,X426)
| agent(X426,skc9,skc12) ),
inference(resolution,[status(thm)],[c501,clause69]) ).
cnf(c314,plain,
( ~ accessible_world(skc10,X417)
| agent(X417,skc13,skc12) ),
inference(resolution,[status(thm)],[clause69,clause91]) ).
cnf(clause68,axiom,
( ~ accessible_world(X240,X239)
| ~ male(X240,X238)
| male(X239,X238) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause68) ).
cnf(c470,plain,
( ~ accessible_world(skc10,X412)
| male(X412,skc15) ),
inference(resolution,[status(thm)],[c467,clause68]) ).
cnf(c469,plain,
( ~ accessible_world(skc10,X411)
| man(X411,skc15) ),
inference(resolution,[status(thm)],[c466,clause67]) ).
cnf(c464,plain,
( ~ accessible_world(skc10,X410)
| vincent_forename(X410,skc14) ),
inference(resolution,[status(thm)],[c457,clause66]) ).
cnf(clause60,axiom,
( ~ accessible_world(X202,X201)
| ~ existent(X202,X200)
| existent(X201,X200) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause60) ).
cnf(c379,plain,
( ~ accessible_world(skc10,X409)
| existent(X409,skc15) ),
inference(resolution,[status(thm)],[c375,clause60]) ).
cnf(clause62,axiom,
( ~ accessible_world(X210,X209)
| ~ living(X210,X208)
| living(X209,X208) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause62) ).
cnf(c377,plain,
( ~ accessible_world(skc10,X408)
| living(X408,skc15) ),
inference(resolution,[status(thm)],[c370,clause62]) ).
cnf(clause59,axiom,
( ~ accessible_world(X199,X198)
| ~ entity(X199,X197)
| entity(X198,X197) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause59) ).
cnf(c374,plain,
( ~ accessible_world(skc10,X403)
| entity(X403,skc15) ),
inference(resolution,[status(thm)],[c368,clause59]) ).
cnf(clause61,axiom,
( ~ accessible_world(X206,X205)
| ~ impartial(X206,X204)
| impartial(X205,X204) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause61) ).
cnf(c371,plain,
( ~ accessible_world(skc10,X402)
| impartial(X402,skc15) ),
inference(resolution,[status(thm)],[c367,clause61]) ).
cnf(clause58,axiom,
( ~ accessible_world(X193,X192)
| ~ organism(X193,X191)
| organism(X192,X191) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause58) ).
cnf(c369,plain,
( ~ accessible_world(skc10,X401)
| organism(X401,skc15) ),
inference(resolution,[status(thm)],[c362,clause58]) ).
cnf(clause63,axiom,
( ~ accessible_world(X214,X213)
| ~ human(X214,X212)
| human(X213,X212) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause63) ).
cnf(c366,plain,
( ~ accessible_world(skc10,X400)
| human(X400,skc15) ),
inference(resolution,[status(thm)],[c361,clause63]) ).
cnf(clause64,axiom,
( ~ accessible_world(X217,X216)
| ~ animate(X217,X215)
| animate(X216,X215) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause64) ).
cnf(c365,plain,
( ~ accessible_world(skc10,X399)
| animate(X399,skc15) ),
inference(resolution,[status(thm)],[c360,clause64]) ).
cnf(c359,plain,
( ~ accessible_world(skc10,X394)
| human_person(X394,skc15) ),
inference(resolution,[status(thm)],[c358,clause57]) ).
cnf(c357,plain,
( ~ accessible_world(skc10,X393)
| existent(X393,skc12) ),
inference(resolution,[status(thm)],[c353,clause60]) ).
cnf(c354,plain,
( ~ accessible_world(skc10,X392)
| living(X392,skc12) ),
inference(resolution,[status(thm)],[c346,clause62]) ).
cnf(c352,plain,
( ~ accessible_world(skc10,X391)
| entity(X391,skc12) ),
inference(resolution,[status(thm)],[c344,clause59]) ).
cnf(c349,plain,
( ~ accessible_world(skc10,X390)
| impartial(X390,skc12) ),
inference(resolution,[status(thm)],[c343,clause61]) ).
cnf(c345,plain,
( ~ accessible_world(skc10,X385)
| organism(X385,skc12) ),
inference(resolution,[status(thm)],[c340,clause58]) ).
cnf(c342,plain,
( ~ accessible_world(skc10,X384)
| human(X384,skc12) ),
inference(resolution,[status(thm)],[c339,clause63]) ).
cnf(c341,plain,
( ~ accessible_world(skc10,X383)
| animate(X383,skc12) ),
inference(resolution,[status(thm)],[c338,clause64]) ).
cnf(c337,plain,
( ~ accessible_world(skc10,X382)
| human_person(X382,skc12) ),
inference(resolution,[status(thm)],[c332,clause57]) ).
cnf(clause65,axiom,
( ~ accessible_world(X222,X221)
| ~ female(X222,X220)
| female(X221,X220) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause65) ).
cnf(c336,plain,
( ~ accessible_world(skc10,X381)
| female(X381,skc12) ),
inference(resolution,[status(thm)],[c330,clause65]) ).
cnf(c331,plain,
( ~ accessible_world(skc10,X376)
| woman(X376,skc12) ),
inference(resolution,[status(thm)],[c329,clause56]) ).
cnf(c328,plain,
( ~ accessible_world(skc10,X375)
| mia_forename(X375,skc11) ),
inference(resolution,[status(thm)],[c324,clause55]) ).
cnf(clause54,axiom,
( ~ accessible_world(X170,X169)
| ~ relname(X170,X168)
| relname(X169,X168) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause54) ).
cnf(c320,plain,
( ~ accessible_world(skc10,X374)
| relname(X374,skc14) ),
inference(resolution,[status(thm)],[c317,clause54]) ).
cnf(c318,plain,
( ~ accessible_world(skc10,X373)
| forename(X373,skc14) ),
inference(resolution,[status(thm)],[c316,clause53]) ).
cnf(c313,plain,
( ~ accessible_world(skc10,X372)
| relname(X372,skc11) ),
inference(resolution,[status(thm)],[c310,clause54]) ).
cnf(c311,plain,
( ~ accessible_world(skc10,X367)
| forename(X367,skc11) ),
inference(resolution,[status(thm)],[c309,clause53]) ).
cnf(c308,plain,
( ~ accessible_world(skc8,X366)
| male(X366,skc15) ),
inference(resolution,[status(thm)],[clause68,c94]) ).
cnf(clause36,axiom,
( ~ female(X74,X73)
| ~ male(X74,X73) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
cnf(c471,plain,
~ female(skc10,skc15),
inference(resolution,[status(thm)],[c467,clause36]) ).
cnf(c298,plain,
( ~ accessible_world(skc8,X355)
| female(X355,skc12) ),
inference(resolution,[status(thm)],[clause65,c85]) ).
cnf(c295,plain,
( ~ accessible_world(skc8,X354)
| animate(X354,skc15) ),
inference(resolution,[status(thm)],[clause64,c88]) ).
cnf(c294,plain,
( ~ accessible_world(skc8,X349)
| animate(X349,skc12) ),
inference(resolution,[status(thm)],[clause64,c84]) ).
cnf(clause52,axiom,
( ~ accessible_world(X157,X156)
| ~ general(X157,X155)
| general(X156,X155) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause52) ).
cnf(c293,plain,
( ~ accessible_world(skc10,X348)
| general(X348,skc14) ),
inference(resolution,[status(thm)],[c290,clause52]) ).
cnf(clause51,axiom,
( ~ accessible_world(X150,X149)
| ~ nonhuman(X150,X148)
| nonhuman(X149,X148) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause51) ).
cnf(c292,plain,
( ~ accessible_world(skc10,X347)
| nonhuman(X347,skc14) ),
inference(resolution,[status(thm)],[c287,clause51]) ).
cnf(clause50,axiom,
( ~ accessible_world(X146,X145)
| ~ abstraction(X146,X144)
| abstraction(X145,X144) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause50) ).
cnf(c288,plain,
( ~ accessible_world(skc10,X346)
| abstraction(X346,skc14) ),
inference(resolution,[status(thm)],[c282,clause50]) ).
cnf(c285,plain,
( ~ accessible_world(skc8,X341)
| human(X341,skc15) ),
inference(resolution,[status(thm)],[clause63,c89]) ).
cnf(c284,plain,
( ~ accessible_world(skc8,X340)
| human(X340,skc12) ),
inference(resolution,[status(thm)],[clause63,c83]) ).
cnf(c283,plain,
( ~ accessible_world(skc10,X339)
| relation(X339,skc14) ),
inference(resolution,[status(thm)],[c281,clause49]) ).
cnf(c280,plain,
( ~ accessible_world(skc10,X334)
| general(X334,skc11) ),
inference(resolution,[status(thm)],[c275,clause52]) ).
cnf(c279,plain,
( ~ accessible_world(skc8,X333)
| living(X333,skc15) ),
inference(resolution,[status(thm)],[clause62,c93]) ).
cnf(c278,plain,
( ~ accessible_world(skc8,X332)
| living(X332,skc12) ),
inference(resolution,[status(thm)],[clause62,c82]) ).
cnf(c277,plain,
( ~ accessible_world(skc10,X327)
| nonhuman(X327,skc11) ),
inference(resolution,[status(thm)],[c272,clause51]) ).
cnf(c273,plain,
( ~ accessible_world(skc10,X326)
| abstraction(X326,skc11) ),
inference(resolution,[status(thm)],[c269,clause50]) ).
cnf(c270,plain,
( ~ accessible_world(skc10,X325)
| relation(X325,skc11) ),
inference(resolution,[status(thm)],[c268,clause49]) ).
cnf(c267,plain,
( ~ accessible_world(skc8,X324)
| impartial(X324,skc12) ),
inference(resolution,[status(thm)],[clause61,c81]) ).
cnf(c266,plain,
( ~ accessible_world(skc8,X319)
| impartial(X319,skc15) ),
inference(resolution,[status(thm)],[clause61,c91]) ).
cnf(c264,plain,
( ~ accessible_world(skc10,X318)
| general(X318,skc10) ),
inference(resolution,[status(thm)],[c259,clause52]) ).
cnf(c263,plain,
( ~ accessible_world(skc8,X317)
| existent(X317,skc15) ),
inference(resolution,[status(thm)],[clause60,c97]) ).
cnf(c262,plain,
( ~ accessible_world(skc8,X312)
| existent(X312,skc12) ),
inference(resolution,[status(thm)],[clause60,c80]) ).
cnf(c261,plain,
( ~ accessible_world(skc10,X311)
| nonhuman(X311,skc10) ),
inference(resolution,[status(thm)],[c256,clause51]) ).
cnf(c257,plain,
( ~ accessible_world(skc10,X310)
| abstraction(X310,skc10) ),
inference(resolution,[status(thm)],[c253,clause50]) ).
cnf(c254,plain,
( ~ accessible_world(skc10,X309)
| relation(X309,skc10) ),
inference(resolution,[status(thm)],[c252,clause49]) ).
cnf(c251,plain,
( ~ accessible_world(skc10,X304)
| proposition(X304,skc10) ),
inference(resolution,[status(thm)],[c248,clause48]) ).
cnf(c250,plain,
( ~ accessible_world(skc8,X303)
| entity(X303,skc15) ),
inference(resolution,[status(thm)],[clause59,c92]) ).
cnf(c249,plain,
( ~ accessible_world(skc8,X302)
| entity(X302,skc12) ),
inference(resolution,[status(thm)],[clause59,c76]) ).
cnf(c246,plain,
( ~ accessible_world(skc10,X297)
| desire_want(X297,skc9) ),
inference(resolution,[status(thm)],[c245,clause47]) ).
cnf(c244,plain,
( ~ accessible_world(skc8,X296)
| organism(X296,skc15) ),
inference(resolution,[status(thm)],[clause58,c90]) ).
cnf(c243,plain,
( ~ accessible_world(skc8,X295)
| organism(X295,skc12) ),
inference(resolution,[status(thm)],[clause58,c75]) ).
cnf(c242,plain,
( ~ accessible_world(skc10,X290)
| present(X290,skc9) ),
inference(resolution,[status(thm)],[c241,clause46]) ).
cnf(c240,plain,
( ~ accessible_world(skc8,X289)
| human_person(X289,skc12) ),
inference(resolution,[status(thm)],[clause57,c74]) ).
cnf(clause37,axiom,
( ~ nonexistent(X76,X75)
| ~ existent(X76,X75) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
cnf(c378,plain,
~ nonexistent(skc10,skc15),
inference(resolution,[status(thm)],[c375,clause37]) ).
cnf(transitivity,axiom,
( X276 != X277
| X277 != X275
| X276 = X275 ),
theory(equality) ).
cnf(c238,plain,
( ~ accessible_world(skc10,X273)
| unisex(X273,skc11) ),
inference(resolution,[status(thm)],[c234,clause45]) ).
cnf(c356,plain,
~ nonexistent(skc10,skc12),
inference(resolution,[status(thm)],[c353,clause37]) ).
cnf(c233,plain,
( ~ accessible_world(skc10,X259)
| unisex(X259,skc10) ),
inference(resolution,[status(thm)],[c229,clause45]) ).
cnf(c227,plain,
( ~ accessible_world(skc8,X253)
| relname(X253,skc14) ),
inference(resolution,[status(thm)],[clause54,c58]) ).
cnf(c226,plain,
( ~ accessible_world(skc8,X252)
| relname(X252,skc11) ),
inference(resolution,[status(thm)],[clause54,c57]) ).
cnf(c225,plain,
( ~ accessible_world(skc10,X247)
| unisex(X247,skc14) ),
inference(resolution,[status(thm)],[c222,clause45]) ).
cnf(c218,plain,
( ~ accessible_world(skc8,X237)
| general(X237,skc10) ),
inference(resolution,[status(thm)],[clause52,c55]) ).
cnf(c217,plain,
( ~ accessible_world(skc8,X236)
| general(X236,skc14) ),
inference(resolution,[status(thm)],[clause52,c70]) ).
cnf(c216,plain,
( ~ accessible_world(skc8,X235)
| general(X235,skc11) ),
inference(resolution,[status(thm)],[clause52,c66]) ).
cnf(c214,plain,
( ~ accessible_world(skc8,X231)
| nonhuman(X231,skc11) ),
inference(resolution,[status(thm)],[clause51,c65]) ).
cnf(c213,plain,
( ~ accessible_world(skc8,X230)
| nonhuman(X230,skc14) ),
inference(resolution,[status(thm)],[clause51,c69]) ).
cnf(c212,plain,
( ~ accessible_world(skc8,X226)
| nonhuman(X226,skc10) ),
inference(resolution,[status(thm)],[clause51,c54]) ).
cnf(c211,plain,
( ~ accessible_world(skc10,X225)
| specific(X225,skc15) ),
inference(resolution,[status(thm)],[c209,clause43]) ).
cnf(c208,plain,
( ~ accessible_world(skc10,X224)
| specific(X224,skc12) ),
inference(resolution,[status(thm)],[c203,clause43]) ).
cnf(c206,plain,
( ~ accessible_world(skc8,X223)
| abstraction(X223,skc14) ),
inference(resolution,[status(thm)],[clause50,c62]) ).
cnf(c205,plain,
( ~ accessible_world(skc8,X219)
| abstraction(X219,skc11) ),
inference(resolution,[status(thm)],[clause50,c61]) ).
cnf(c204,plain,
( ~ accessible_world(skc8,X218)
| abstraction(X218,skc10) ),
inference(resolution,[status(thm)],[clause50,c51]) ).
cnf(clause35,axiom,
( ~ human(X72,X71)
| ~ nonhuman(X72,X71) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
cnf(c291,plain,
~ human(skc10,skc14),
inference(resolution,[status(thm)],[c287,clause35]) ).
cnf(c276,plain,
~ human(skc10,skc11),
inference(resolution,[status(thm)],[c272,clause35]) ).
cnf(c199,plain,
( ~ accessible_world(skc8,X203)
| relation(X203,skc10) ),
inference(resolution,[status(thm)],[clause49,c50]) ).
cnf(c260,plain,
~ human(skc10,skc10),
inference(resolution,[status(thm)],[c256,clause35]) ).
cnf(clause42,axiom,
( ~ accessible_world(X100,X99)
| ~ singleton(X100,X98)
| singleton(X99,X98) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause42) ).
cnf(c191,plain,
( ~ accessible_world(skc10,X194)
| singleton(X194,skc14) ),
inference(resolution,[status(thm)],[c190,clause42]) ).
cnf(c189,plain,
( ~ accessible_world(skc10,X190)
| thing(X190,skc14) ),
inference(resolution,[status(thm)],[c188,clause41]) ).
cnf(c186,plain,
( ~ accessible_world(skc10,X188)
| present(X188,skc13) ),
inference(resolution,[status(thm)],[clause46,clause78]) ).
cnf(c185,plain,
( ~ accessible_world(skc10,X187)
| singleton(X187,skc12) ),
inference(resolution,[status(thm)],[c184,clause42]) ).
cnf(c183,plain,
( ~ accessible_world(skc10,X183)
| thing(X183,skc12) ),
inference(resolution,[status(thm)],[c182,clause41]) ).
cnf(c181,plain,
( ~ accessible_world(skc10,X182)
| singleton(X182,skc10) ),
inference(resolution,[status(thm)],[c174,clause42]) ).
cnf(clause33,axiom,
( ~ female(X68,X67)
| ~ unisex(X68,X67) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
cnf(c237,plain,
~ female(skc10,skc11),
inference(resolution,[status(thm)],[c234,clause33]) ).
cnf(clause32,axiom,
( ~ male(X66,X65)
| ~ unisex(X66,X65) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
cnf(c236,plain,
~ male(skc10,skc11),
inference(resolution,[status(thm)],[c234,clause32]) ).
cnf(c179,plain,
( ~ accessible_world(skc10,X177)
| unisex(X177,skc13) ),
inference(resolution,[status(thm)],[clause45,c42]) ).
cnf(c232,plain,
~ female(skc10,skc10),
inference(resolution,[status(thm)],[c229,clause33]) ).
cnf(c231,plain,
~ male(skc10,skc10),
inference(resolution,[status(thm)],[c229,clause32]) ).
cnf(c177,plain,
( ~ accessible_world(skc10,X172)
| unisex(X172,skc9) ),
inference(resolution,[status(thm)],[clause45,c131]) ).
cnf(c176,plain,
( ~ accessible_world(skc8,X171)
| unisex(X171,skc9) ),
inference(resolution,[status(thm)],[clause45,c48]) ).
cnf(c224,plain,
~ female(skc10,skc14),
inference(resolution,[status(thm)],[c222,clause33]) ).
cnf(c223,plain,
~ male(skc10,skc14),
inference(resolution,[status(thm)],[c222,clause32]) ).
cnf(c173,plain,
( ~ accessible_world(skc10,X166)
| thing(X166,skc10) ),
inference(resolution,[status(thm)],[c172,clause41]) ).
cnf(c171,plain,
( ~ accessible_world(skc10,X165)
| singleton(X165,skc15) ),
inference(resolution,[status(thm)],[c170,clause42]) ).
cnf(c169,plain,
( ~ accessible_world(skc10,X161)
| thing(X161,skc15) ),
inference(resolution,[status(thm)],[c168,clause41]) ).
cnf(clause44,axiom,
( ~ accessible_world(X112,X111)
| ~ nonexistent(X112,X110)
| nonexistent(X111,X110) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause44) ).
cnf(c167,plain,
( ~ accessible_world(skc10,X160)
| nonexistent(X160,skc13) ),
inference(resolution,[status(thm)],[clause44,c41]) ).
cnf(c166,plain,
( ~ accessible_world(skc8,X159)
| nonexistent(X159,skc9) ),
inference(resolution,[status(thm)],[clause44,c45]) ).
cnf(c165,plain,
( ~ accessible_world(skc10,X158)
| nonexistent(X158,skc9) ),
inference(resolution,[status(thm)],[clause44,c132]) ).
cnf(c163,plain,
( ~ accessible_world(skc10,X154)
| singleton(X154,skc11) ),
inference(resolution,[status(thm)],[c162,clause42]) ).
cnf(c161,plain,
( ~ accessible_world(skc10,X153)
| thing(X153,skc11) ),
inference(resolution,[status(thm)],[c160,clause41]) ).
cnf(c159,plain,
( ~ accessible_world(skc8,X152)
| specific(X152,skc9) ),
inference(resolution,[status(thm)],[clause43,c46]) ).
cnf(c158,plain,
( ~ accessible_world(skc10,X151)
| specific(X151,skc13) ),
inference(resolution,[status(thm)],[clause43,c40]) ).
cnf(clause34,axiom,
( ~ general(X70,X69)
| ~ specific(X70,X69) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
cnf(c210,plain,
~ general(skc10,skc15),
inference(resolution,[status(thm)],[c209,clause34]) ).
cnf(c207,plain,
~ general(skc10,skc12),
inference(resolution,[status(thm)],[c203,clause34]) ).
cnf(c155,plain,
( ~ accessible_world(skc10,X142)
| specific(X142,skc9) ),
inference(resolution,[status(thm)],[clause43,c133]) ).
cnf(c153,plain,
( ~ accessible_world(skc10,X141)
| singleton(X141,skc13) ),
inference(resolution,[status(thm)],[clause42,c39]) ).
cnf(c152,plain,
( ~ accessible_world(skc8,X140)
| singleton(X140,skc15) ),
inference(resolution,[status(thm)],[clause42,c98]) ).
cnf(c151,plain,
( ~ accessible_world(skc8,X136)
| singleton(X136,skc11) ),
inference(resolution,[status(thm)],[clause42,c71]) ).
cnf(c150,plain,
( ~ accessible_world(skc8,X135)
| singleton(X135,skc14) ),
inference(resolution,[status(thm)],[clause42,c73]) ).
cnf(c149,plain,
( ~ accessible_world(skc8,X131)
| singleton(X131,skc12) ),
inference(resolution,[status(thm)],[clause42,c79]) ).
cnf(c148,plain,
( ~ accessible_world(skc8,X130)
| singleton(X130,skc10) ),
inference(resolution,[status(thm)],[clause42,c53]) ).
cnf(c147,plain,
( ~ accessible_world(skc8,X129)
| singleton(X129,skc9) ),
inference(resolution,[status(thm)],[clause42,c49]) ).
cnf(c146,plain,
( ~ accessible_world(skc10,X125)
| singleton(X125,skc9) ),
inference(resolution,[status(thm)],[clause42,c134]) ).
cnf(c144,plain,
( ~ accessible_world(skc10,X124)
| thing(X124,skc9) ),
inference(resolution,[status(thm)],[clause41,c130]) ).
cnf(c141,plain,
( ~ accessible_world(skc10,X118)
| thing(X118,skc13) ),
inference(resolution,[status(thm)],[clause41,c38]) ).
cnf(c138,plain,
( ~ accessible_world(skc8,X109)
| thing(X109,skc9) ),
inference(resolution,[status(thm)],[clause41,c47]) ).
cnf(clause40,axiom,
( ~ accessible_world(X94,X93)
| ~ eventuality(X94,X92)
| eventuality(X93,X92) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause40) ).
cnf(c129,plain,
( ~ accessible_world(skc10,X104)
| eventuality(X104,skc9) ),
inference(resolution,[status(thm)],[c128,clause40]) ).
cnf(c127,plain,
( ~ accessible_world(skc10,X103)
| event(X103,skc9) ),
inference(resolution,[status(thm)],[c124,clause39]) ).
cnf(c126,plain,
( ~ accessible_world(skc8,X102)
| eventuality(X102,skc9) ),
inference(resolution,[status(thm)],[clause40,c44]) ).
cnf(c125,plain,
( ~ accessible_world(skc10,X101)
| eventuality(X101,skc13) ),
inference(resolution,[status(thm)],[clause40,c37]) ).
cnf(c145,plain,
~ general(skc10,skc9),
inference(resolution,[status(thm)],[c133,clause34]) ).
cnf(c136,plain,
~ female(skc10,skc9),
inference(resolution,[status(thm)],[c131,clause33]) ).
cnf(c135,plain,
~ male(skc10,skc9),
inference(resolution,[status(thm)],[c131,clause32]) ).
cnf(c121,plain,
( ~ accessible_world(skc10,X90)
| event(X90,skc13) ),
inference(resolution,[status(thm)],[clause39,clause76]) ).
cnf(clause38,axiom,
( ~ accessible_world(X79,X78)
| ~ dance(X79,X77)
| dance(X78,X77) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
cnf(c119,plain,
( ~ accessible_world(skc10,X89)
| dance(X89,skc13) ),
inference(resolution,[status(thm)],[clause38,clause79]) ).
cnf(c35,axiom,
( X86 != X87
| ~ actual_world(X86)
| actual_world(X87) ),
theory(equality) ).
cnf(symmetry,axiom,
( X80 != X81
| X81 = X80 ),
theory(equality) ).
cnf(c118,plain,
~ nonexistent(skc8,skc15),
inference(resolution,[status(thm)],[clause37,c97]) ).
cnf(c117,plain,
~ nonexistent(skc8,skc12),
inference(resolution,[status(thm)],[clause37,c80]) ).
cnf(c116,plain,
~ female(skc8,skc15),
inference(resolution,[status(thm)],[clause36,c94]) ).
cnf(c115,plain,
~ human(skc8,skc11),
inference(resolution,[status(thm)],[clause35,c65]) ).
cnf(c114,plain,
~ human(skc8,skc14),
inference(resolution,[status(thm)],[clause35,c69]) ).
cnf(c113,plain,
~ human(skc8,skc10),
inference(resolution,[status(thm)],[clause35,c54]) ).
cnf(c112,plain,
~ general(skc8,skc9),
inference(resolution,[status(thm)],[clause34,c46]) ).
cnf(c111,plain,
~ general(skc8,skc12),
inference(resolution,[status(thm)],[clause34,c78]) ).
cnf(c110,plain,
~ general(skc10,skc13),
inference(resolution,[status(thm)],[clause34,c40]) ).
cnf(c109,plain,
~ general(skc8,skc15),
inference(resolution,[status(thm)],[clause34,c96]) ).
cnf(c108,plain,
~ female(skc8,skc11),
inference(resolution,[status(thm)],[clause33,c64]) ).
cnf(c107,plain,
~ female(skc10,skc13),
inference(resolution,[status(thm)],[clause33,c42]) ).
cnf(c106,plain,
~ female(skc8,skc10),
inference(resolution,[status(thm)],[clause33,c56]) ).
cnf(c105,plain,
~ female(skc8,skc9),
inference(resolution,[status(thm)],[clause33,c48]) ).
cnf(c104,plain,
~ female(skc8,skc14),
inference(resolution,[status(thm)],[clause33,c68]) ).
cnf(c103,plain,
~ male(skc8,skc11),
inference(resolution,[status(thm)],[clause32,c64]) ).
cnf(c102,plain,
~ male(skc10,skc13),
inference(resolution,[status(thm)],[clause32,c42]) ).
cnf(c101,plain,
~ male(skc8,skc10),
inference(resolution,[status(thm)],[clause32,c56]) ).
cnf(c100,plain,
~ male(skc8,skc9),
inference(resolution,[status(thm)],[clause32,c48]) ).
cnf(c99,plain,
~ male(skc8,skc14),
inference(resolution,[status(thm)],[clause32,c68]) ).
cnf(clause29,axiom,
( ~ vincent_forename(X60,X59)
| forename(X60,X59) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
cnf(clause17,axiom,
( ~ mia_forename(X36,X35)
| forename(X36,X35) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
cnf(clause1,axiom,
( ~ dance(X4,X3)
| event(X4,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
cnf(clause74,negated_conjecture,
actual_world(skc8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause74) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NLP024-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 : n007.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:47:53 EDT 2024
% 0.13/0.34 % CPUTime :
% 1.00/1.20 % Version: 1.5
% 1.00/1.20 % SZS status Satisfiable
% 1.00/1.20 % SZS output start Saturation
% See solution above
% 1.00/1.21
% 1.00/1.21 % Initial clauses : 132
% 1.00/1.21 % Processed clauses : 756
% 1.00/1.21 % Factors computed : 12
% 1.00/1.21 % Resolvents computed: 837
% 1.00/1.21 % Tautologies deleted: 3
% 1.00/1.21 % Forward subsumed : 222
% 1.00/1.21 % Backward subsumed : 0
% 1.00/1.21 % -------- CPU Time ---------
% 1.00/1.21 % User time : 0.844 s
% 1.00/1.21 % System time : 0.029 s
% 1.00/1.21 % Total time : 0.873 s
%------------------------------------------------------------------------------