%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP103-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:34:04 EDT 2024
% Result : Satisfiable 0.55s 0.78s
% Output : Saturation 0.55s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause10,negated_conjecture,
( ~ ssSkC0
| coffee(skc8,skc9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(clause1,negated_conjecture,
actual_world(skc20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
cnf(clause7,negated_conjecture,
( ssSkC0
| coffee(skc20,skc25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
cnf(clause3,negated_conjecture,
( ssSkC0
| event(skc20,skc21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(clause4,negated_conjecture,
( ssSkC0
| past(skc20,skc21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
cnf(clause5,negated_conjecture,
( ssSkC0
| nonreflexive(skc20,skc21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
cnf(clause6,negated_conjecture,
( ssSkC0
| drink(skc20,skc21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
cnf(clause8,negated_conjecture,
( ssSkC0
| human_person(skc20,skc22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
cnf(clause9,negated_conjecture,
( ssSkC0
| restaurant(skc20,skc23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
cnf(clause12,negated_conjecture,
( ssSkC0
| patient(skc20,skc21,skc25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
cnf(clause13,negated_conjecture,
( ssSkC0
| agent(skc20,skc21,skc22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
cnf(clause33,negated_conjecture,
( ~ coffee(X30,X31)
| ~ restaurant(X30,X32)
| ~ actual_world(X30)
| ssSkC0
| customer(X30,skf20(X30,X28,X29)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
cnf(c27,plain,
( ~ coffee(skc20,X34)
| ~ actual_world(skc20)
| ssSkC0
| customer(skc20,skf20(skc20,X35,X33)) ),
inference(resolution,[status(thm)],[clause33,clause9]) ).
cnf(c31,plain,
( ~ actual_world(skc20)
| ssSkC0
| customer(skc20,skf20(skc20,X37,X36)) ),
inference(resolution,[status(thm)],[c27,clause7]) ).
cnf(c33,plain,
( ssSkC0
| customer(skc20,skf20(skc20,X39,X40)) ),
inference(resolution,[status(thm)],[c31,clause1]) ).
cnf(clause17,negated_conjecture,
( ~ in(skc20,X8,skc23)
| ~ customer(skc20,X8)
| ssSkC0
| see(skc20,skf16(X9)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
cnf(clause34,negated_conjecture,
( ~ coffee(X46,X49)
| ~ restaurant(X46,X47)
| ~ actual_world(X46)
| ssSkC0
| in(X46,skf20(X46,X47,X48),X47) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
cnf(c47,plain,
( ~ coffee(skc20,X70)
| ~ actual_world(skc20)
| ssSkC0
| in(skc20,skf20(skc20,skc23,X69),skc23) ),
inference(resolution,[status(thm)],[clause34,clause9]) ).
cnf(c54,plain,
( ~ actual_world(skc20)
| ssSkC0
| in(skc20,skf20(skc20,skc23,X71),skc23) ),
inference(resolution,[status(thm)],[c47,clause7]) ).
cnf(c56,plain,
( ssSkC0
| in(skc20,skf20(skc20,skc23,X72),skc23) ),
inference(resolution,[status(thm)],[c54,clause1]) ).
cnf(c60,plain,
( ssSkC0
| ~ customer(skc20,skf20(skc20,skc23,X94))
| see(skc20,skf16(X95)) ),
inference(resolution,[status(thm)],[c56,clause17]) ).
cnf(c91,plain,
( ssSkC0
| see(skc20,skf16(X96)) ),
inference(resolution,[status(thm)],[c60,c33]) ).
cnf(clause16,negated_conjecture,
( ~ in(skc20,X6,skc23)
| ~ customer(skc20,X6)
| ssSkC0
| nonreflexive(skc20,skf16(X7)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(c59,plain,
( ssSkC0
| ~ customer(skc20,skf20(skc20,skc23,X81))
| nonreflexive(skc20,skf16(X82)) ),
inference(resolution,[status(thm)],[c56,clause16]) ).
cnf(c83,plain,
( ssSkC0
| nonreflexive(skc20,skf16(X83)) ),
inference(resolution,[status(thm)],[c59,c33]) ).
cnf(clause15,negated_conjecture,
( ~ in(skc20,X4,skc23)
| ~ customer(skc20,X4)
| ssSkC0
| past(skc20,skf16(X5)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
cnf(c64,plain,
( ssSkC0
| ~ customer(skc20,skf20(skc20,skc23,X118))
| past(skc20,skf16(X117)) ),
inference(resolution,[status(thm)],[c56,clause15]) ).
cnf(c105,plain,
( ssSkC0
| past(skc20,skf16(X119)) ),
inference(resolution,[status(thm)],[c64,c33]) ).
cnf(clause14,negated_conjecture,
( ~ in(skc20,X2,skc23)
| ~ customer(skc20,X2)
| ssSkC0
| event(skc20,skf16(X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
cnf(c62,plain,
( ssSkC0
| ~ customer(skc20,skf20(skc20,skc23,X107))
| event(skc20,skf16(X108)) ),
inference(resolution,[status(thm)],[c56,clause14]) ).
cnf(c98,plain,
( ssSkC0
| event(skc20,skf16(X109)) ),
inference(resolution,[status(thm)],[c62,c33]) ).
cnf(clause28,negated_conjecture,
( ~ in(skc20,X50,skc23)
| ~ customer(skc20,X50)
| ssSkC0
| patient(skc20,skf16(X51),skc22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
cnf(c63,plain,
( ssSkC0
| ~ customer(skc20,skf20(skc20,skc23,X128))
| patient(skc20,skf16(X127),skc22) ),
inference(resolution,[status(thm)],[c56,clause28]) ).
cnf(c112,plain,
( ssSkC0
| patient(skc20,skf16(X132),skc22) ),
inference(resolution,[status(thm)],[c63,c33]) ).
cnf(clause37,negated_conjecture,
( ~ coffee(X89,X91)
| ~ see(X89,X92)
| ~ nonreflexive(X89,X92)
| ~ past(X89,X92)
| ~ agent(X89,X92,skf20(X89,X87,X91))
| ~ event(X89,X92)
| ~ event(X89,X88)
| ~ patient(X89,X88,X91)
| ~ past(X89,X88)
| ~ nonreflexive(X89,X88)
| ~ drink(X89,X88)
| ~ patient(X89,X92,X90)
| ~ agent(X89,X88,X90)
| ~ human_person(X89,X90)
| ~ restaurant(X89,X87)
| ~ actual_world(X89)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
cnf(clause27,negated_conjecture,
( ~ in(skc20,X38,skc23)
| ~ customer(skc20,X38)
| ssSkC0
| agent(skc20,skf16(X38),X38) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
cnf(c61,plain,
( ssSkC0
| ~ customer(skc20,skf20(skc20,skc23,X250))
| agent(skc20,skf16(skf20(skc20,skc23,X250)),skf20(skc20,skc23,X250)) ),
inference(resolution,[status(thm)],[c56,clause27]) ).
cnf(c119,plain,
( ssSkC0
| agent(skc20,skf16(skf20(skc20,skc23,X251)),skf20(skc20,skc23,X251)) ),
inference(resolution,[status(thm)],[c61,c33]) ).
cnf(c124,plain,
( ssSkC0
| ~ coffee(skc20,X315)
| ~ see(skc20,skf16(skf20(skc20,skc23,X315)))
| ~ nonreflexive(skc20,skf16(skf20(skc20,skc23,X315)))
| ~ past(skc20,skf16(skf20(skc20,skc23,X315)))
| ~ event(skc20,skf16(skf20(skc20,skc23,X315)))
| ~ event(skc20,X317)
| ~ patient(skc20,X317,X315)
| ~ past(skc20,X317)
| ~ nonreflexive(skc20,X317)
| ~ drink(skc20,X317)
| ~ patient(skc20,skf16(skf20(skc20,skc23,X315)),X316)
| ~ agent(skc20,X317,X316)
| ~ human_person(skc20,X316)
| ~ restaurant(skc20,skc23)
| ~ actual_world(skc20) ),
inference(resolution,[status(thm)],[c119,clause37]) ).
cnf(c136,plain,
( ssSkC0
| ~ coffee(skc20,X319)
| ~ see(skc20,skf16(skf20(skc20,skc23,X319)))
| ~ nonreflexive(skc20,skf16(skf20(skc20,skc23,X319)))
| ~ past(skc20,skf16(skf20(skc20,skc23,X319)))
| ~ event(skc20,skf16(skf20(skc20,skc23,X319)))
| ~ event(skc20,X318)
| ~ patient(skc20,X318,X319)
| ~ past(skc20,X318)
| ~ nonreflexive(skc20,X318)
| ~ drink(skc20,X318)
| ~ agent(skc20,X318,skc22)
| ~ human_person(skc20,skc22)
| ~ restaurant(skc20,skc23)
| ~ actual_world(skc20) ),
inference(resolution,[status(thm)],[c124,c112]) ).
cnf(c141,plain,
( ssSkC0
| ~ coffee(skc20,X321)
| ~ see(skc20,skf16(skf20(skc20,skc23,X321)))
| ~ nonreflexive(skc20,skf16(skf20(skc20,skc23,X321)))
| ~ past(skc20,skf16(skf20(skc20,skc23,X321)))
| ~ event(skc20,X320)
| ~ patient(skc20,X320,X321)
| ~ past(skc20,X320)
| ~ nonreflexive(skc20,X320)
| ~ drink(skc20,X320)
| ~ agent(skc20,X320,skc22)
| ~ human_person(skc20,skc22)
| ~ restaurant(skc20,skc23)
| ~ actual_world(skc20) ),
inference(resolution,[status(thm)],[c136,c98]) ).
cnf(c143,plain,
( ssSkC0
| ~ coffee(skc20,X322)
| ~ see(skc20,skf16(skf20(skc20,skc23,X322)))
| ~ nonreflexive(skc20,skf16(skf20(skc20,skc23,X322)))
| ~ event(skc20,X323)
| ~ patient(skc20,X323,X322)
| ~ past(skc20,X323)
| ~ nonreflexive(skc20,X323)
| ~ drink(skc20,X323)
| ~ agent(skc20,X323,skc22)
| ~ human_person(skc20,skc22)
| ~ restaurant(skc20,skc23)
| ~ actual_world(skc20) ),
inference(resolution,[status(thm)],[c141,c105]) ).
cnf(c148,plain,
( ssSkC0
| ~ coffee(skc20,X324)
| ~ see(skc20,skf16(skf20(skc20,skc23,X324)))
| ~ event(skc20,X325)
| ~ patient(skc20,X325,X324)
| ~ past(skc20,X325)
| ~ nonreflexive(skc20,X325)
| ~ drink(skc20,X325)
| ~ agent(skc20,X325,skc22)
| ~ human_person(skc20,skc22)
| ~ restaurant(skc20,skc23)
| ~ actual_world(skc20) ),
inference(resolution,[status(thm)],[c143,c83]) ).
cnf(c152,plain,
( ssSkC0
| ~ coffee(skc20,X327)
| ~ event(skc20,X326)
| ~ patient(skc20,X326,X327)
| ~ past(skc20,X326)
| ~ nonreflexive(skc20,X326)
| ~ drink(skc20,X326)
| ~ agent(skc20,X326,skc22)
| ~ human_person(skc20,skc22)
| ~ restaurant(skc20,skc23)
| ~ actual_world(skc20) ),
inference(resolution,[status(thm)],[c148,c91]) ).
cnf(c153,plain,
( ssSkC0
| ~ coffee(skc20,X331)
| ~ event(skc20,skc21)
| ~ patient(skc20,skc21,X331)
| ~ past(skc20,skc21)
| ~ nonreflexive(skc20,skc21)
| ~ drink(skc20,skc21)
| ~ human_person(skc20,skc22)
| ~ restaurant(skc20,skc23)
| ~ actual_world(skc20) ),
inference(resolution,[status(thm)],[c152,clause13]) ).
cnf(c157,plain,
( ssSkC0
| ~ coffee(skc20,skc25)
| ~ event(skc20,skc21)
| ~ past(skc20,skc21)
| ~ nonreflexive(skc20,skc21)
| ~ drink(skc20,skc21)
| ~ human_person(skc20,skc22)
| ~ restaurant(skc20,skc23)
| ~ actual_world(skc20) ),
inference(resolution,[status(thm)],[c153,clause12]) ).
cnf(c160,plain,
( ssSkC0
| ~ coffee(skc20,skc25)
| ~ event(skc20,skc21)
| ~ past(skc20,skc21)
| ~ nonreflexive(skc20,skc21)
| ~ drink(skc20,skc21)
| ~ human_person(skc20,skc22)
| ~ actual_world(skc20) ),
inference(resolution,[status(thm)],[c157,clause9]) ).
cnf(c163,plain,
( ssSkC0
| ~ coffee(skc20,skc25)
| ~ event(skc20,skc21)
| ~ past(skc20,skc21)
| ~ nonreflexive(skc20,skc21)
| ~ drink(skc20,skc21)
| ~ actual_world(skc20) ),
inference(resolution,[status(thm)],[c160,clause8]) ).
cnf(c167,plain,
( ssSkC0
| ~ coffee(skc20,skc25)
| ~ event(skc20,skc21)
| ~ past(skc20,skc21)
| ~ nonreflexive(skc20,skc21)
| ~ actual_world(skc20) ),
inference(resolution,[status(thm)],[c163,clause6]) ).
cnf(c170,plain,
( ssSkC0
| ~ coffee(skc20,skc25)
| ~ event(skc20,skc21)
| ~ past(skc20,skc21)
| ~ actual_world(skc20) ),
inference(resolution,[status(thm)],[c167,clause5]) ).
cnf(c172,plain,
( ssSkC0
| ~ coffee(skc20,skc25)
| ~ event(skc20,skc21)
| ~ actual_world(skc20) ),
inference(resolution,[status(thm)],[c170,clause4]) ).
cnf(c176,plain,
( ssSkC0
| ~ coffee(skc20,skc25)
| ~ actual_world(skc20) ),
inference(resolution,[status(thm)],[c172,clause3]) ).
cnf(c178,plain,
( ssSkC0
| ~ actual_world(skc20) ),
inference(resolution,[status(thm)],[c176,clause7]) ).
cnf(c180,plain,
ssSkC0,
inference(resolution,[status(thm)],[c178,clause1]) ).
cnf(c182,plain,
coffee(skc8,skc9),
inference(resolution,[status(thm)],[c180,clause10]) ).
cnf(clause11,negated_conjecture,
( ~ ssSkC0
| restaurant(skc8,skc10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(c181,plain,
restaurant(skc8,skc10),
inference(resolution,[status(thm)],[c180,clause11]) ).
cnf(clause38,negated_conjecture,
( ~ event(X101,X103)
| ~ past(X101,X103)
| ~ nonreflexive(X101,X103)
| ~ drink(X101,X103)
| ~ patient(X101,X103,X104)
| ~ coffee(X101,X104)
| ~ agent(X101,X103,X99)
| ~ human_person(X101,X99)
| ~ restaurant(X101,X100)
| ~ see(X101,X102)
| ~ nonreflexive(X101,X102)
| ~ past(X101,X102)
| ~ patient(X101,X102,X99)
| ~ agent(X101,X102,skf12(X101,X100,X99))
| ~ event(X101,X102)
| ~ actual_world(X101)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
cnf(clause36,negated_conjecture,
( ~ event(X77,X79)
| ~ past(X77,X79)
| ~ nonreflexive(X77,X79)
| ~ drink(X77,X79)
| ~ patient(X77,X79,X80)
| ~ coffee(X77,X80)
| ~ agent(X77,X79,X75)
| ~ human_person(X77,X75)
| ~ restaurant(X77,X76)
| ~ actual_world(X77)
| ~ ssSkC0
| in(X77,skf12(X77,X76,X78),X76) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
cnf(clause35,negated_conjecture,
( ~ event(X64,X67)
| ~ past(X64,X67)
| ~ nonreflexive(X64,X67)
| ~ drink(X64,X67)
| ~ patient(X64,X67,X68)
| ~ coffee(X64,X68)
| ~ agent(X64,X67,X62)
| ~ human_person(X64,X62)
| ~ restaurant(X64,X63)
| ~ actual_world(X64)
| ~ ssSkC0
| customer(X64,skf12(X64,X65,X66)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
cnf(clause32,negated_conjecture,
( ~ in(skc8,X60,skc10)
| ~ customer(skc8,X60)
| ~ ssSkC0
| patient(skc8,skf8(X61),skf10(X61)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
cnf(clause31,negated_conjecture,
( ~ in(skc8,X58,skc10)
| ~ customer(skc8,X58)
| ~ ssSkC0
| agent(skc8,skf9(X59),skf10(X59)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
cnf(clause29,negated_conjecture,
( ~ in(skc8,X56,skc10)
| ~ customer(skc8,X56)
| ~ ssSkC0
| patient(skc8,skf9(X57),skc9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
cnf(clause30,negated_conjecture,
( ~ in(skc8,X45,skc10)
| ~ customer(skc8,X45)
| ~ ssSkC0
| agent(skc8,skf8(X45),X45) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
cnf(clause26,negated_conjecture,
( ~ in(skc8,X26,skc10)
| ~ customer(skc8,X26)
| ~ ssSkC0
| see(skc8,skf8(X27)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
cnf(clause25,negated_conjecture,
( ~ in(skc8,X24,skc10)
| ~ customer(skc8,X24)
| ~ ssSkC0
| nonreflexive(skc8,skf8(X25)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
cnf(clause24,negated_conjecture,
( ~ in(skc8,X22,skc10)
| ~ customer(skc8,X22)
| ~ ssSkC0
| past(skc8,skf8(X23)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
cnf(clause23,negated_conjecture,
( ~ in(skc8,X20,skc10)
| ~ customer(skc8,X20)
| ~ ssSkC0
| event(skc8,skf8(X21)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
cnf(clause22,negated_conjecture,
( ~ in(skc8,X18,skc10)
| ~ customer(skc8,X18)
| ~ ssSkC0
| event(skc8,skf9(X19)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
cnf(clause21,negated_conjecture,
( ~ in(skc8,X16,skc10)
| ~ customer(skc8,X16)
| ~ ssSkC0
| past(skc8,skf9(X17)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
cnf(clause20,negated_conjecture,
( ~ in(skc8,X14,skc10)
| ~ customer(skc8,X14)
| ~ ssSkC0
| nonreflexive(skc8,skf9(X15)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
cnf(clause19,negated_conjecture,
( ~ in(skc8,X12,skc10)
| ~ customer(skc8,X12)
| ~ ssSkC0
| drink(skc8,skf9(X13)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
cnf(clause18,negated_conjecture,
( ~ in(skc8,X10,skc10)
| ~ customer(skc8,X10)
| ~ ssSkC0
| human_person(skc8,skf10(X11)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
cnf(clause2,negated_conjecture,
actual_world(skc8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : NLP103-1 : TPTP v8.1.2. Released v2.4.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n023.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed May 8 13:37:08 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.55/0.78 % Version: 1.5
% 0.55/0.78 % SZS status Satisfiable
% 0.55/0.78 % SZS output start Saturation
% See solution above
% 0.55/0.78
% 0.55/0.78 % Initial clauses : 38
% 0.55/0.78 % Processed clauses : 109
% 0.55/0.78 % Factors computed : 5
% 0.55/0.78 % Resolvents computed: 178
% 0.55/0.78 % Tautologies deleted: 4
% 0.55/0.78 % Forward subsumed : 108
% 0.55/0.78 % Backward subsumed : 88
% 0.55/0.78 % -------- CPU Time ---------
% 0.55/0.78 % User time : 0.423 s
% 0.55/0.78 % System time : 0.013 s
% 0.55/0.78 % Total time : 0.436 s
%------------------------------------------------------------------------------