%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP102-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.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.43s 0.60s
% Output : Saturation 0.43s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(clause38,negated_conjecture,
( ~ event(X118,X121)
| ~ past(X118,X121)
| ~ nonreflexive(X118,X121)
| ~ drink(X118,X121)
| ~ patient(X118,X121,X123)
| ~ coffee(X118,X123)
| ~ agent(X118,X121,X119)
| ~ human_person(X118,X119)
| ~ restaurant(X118,X120)
| ~ see(X118,X122)
| ~ nonreflexive(X118,X122)
| ~ past(X118,X122)
| ~ patient(X118,X122,X119)
| ~ agent(X118,X122,skf13(X118,X120,X119))
| ~ event(X118,X122)
| ~ actual_world(X118)
| ~ ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
cnf(clause37,negated_conjecture,
( ~ see(X107,X110)
| ~ nonreflexive(X107,X110)
| ~ past(X107,X110)
| ~ agent(X107,X110,skf25(X107,X111))
| ~ event(X107,X110)
| ~ event(X107,X108)
| ~ patient(X107,X108,X111)
| ~ past(X107,X108)
| ~ nonreflexive(X107,X108)
| ~ drink(X107,X108)
| ~ patient(X107,X110,X109)
| ~ agent(X107,X108,X109)
| ~ human_person(X107,X109)
| ~ coffee(X107,X111)
| ~ actual_world(X107)
| ssSkC0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
cnf(c61,plain,
( ~ see(X116,X115)
| ~ nonreflexive(X116,X115)
| ~ past(X116,X115)
| ~ agent(X116,X115,skf25(X116,X117))
| ~ event(X116,X115)
| ~ patient(X116,X115,X117)
| ~ drink(X116,X115)
| ~ patient(X116,X115,skf25(X116,X117))
| ~ human_person(X116,skf25(X116,X117))
| ~ coffee(X116,X117)
| ~ actual_world(X116)
| ssSkC0 ),
inference(factor,[status(thm)],[clause37]) ).
cnf(clause36,negated_conjecture,
( ~ event(X100,X103)
| ~ past(X100,X103)
| ~ nonreflexive(X100,X103)
| ~ drink(X100,X103)
| ~ patient(X100,X103,X105)
| ~ coffee(X100,X105)
| ~ agent(X100,X103,X101)
| ~ human_person(X100,X101)
| ~ restaurant(X100,X102)
| ~ actual_world(X100)
| ~ ssSkC0
| in(X100,skf13(X100,X102,X104),X102) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
cnf(clause35,negated_conjecture,
( ~ event(X93,X96)
| ~ past(X93,X96)
| ~ nonreflexive(X93,X96)
| ~ drink(X93,X96)
| ~ patient(X93,X96,X99)
| ~ coffee(X93,X99)
| ~ agent(X93,X96,X94)
| ~ human_person(X93,X94)
| ~ restaurant(X93,X95)
| ~ actual_world(X93)
| ~ ssSkC0
| customer(X93,skf13(X93,X97,X98)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
cnf(clause34,negated_conjecture,
( ~ restaurant(skc7,X90)
| ~ in(skc7,X92,X90)
| ~ customer(skc7,X92)
| ~ ssSkC0
| agent(skc7,skf10(X91),skf11(X91)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
cnf(clause33,negated_conjecture,
( ~ restaurant(skc7,X87)
| ~ in(skc7,X89,X87)
| ~ customer(skc7,X89)
| ~ ssSkC0
| patient(skc7,skf9(X88),skf11(X88)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
cnf(clause32,negated_conjecture,
( ~ restaurant(skc7,X84)
| ~ in(skc7,X86,X84)
| ~ customer(skc7,X86)
| ~ ssSkC0
| patient(skc7,skf10(X85),skc8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
cnf(clause31,negated_conjecture,
( ~ restaurant(skc7,X82)
| ~ in(skc7,X83,X82)
| ~ customer(skc7,X83)
| ~ ssSkC0
| agent(skc7,skf9(X83),X83) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
cnf(clause30,negated_conjecture,
( ~ restaurant(skc7,X79)
| ~ in(skc7,X81,X79)
| ~ customer(skc7,X81)
| ~ ssSkC0
| human_person(skc7,skf11(X80)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
cnf(clause29,negated_conjecture,
( ~ restaurant(skc7,X76)
| ~ in(skc7,X78,X76)
| ~ customer(skc7,X78)
| ~ ssSkC0
| drink(skc7,skf10(X77)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
cnf(clause28,negated_conjecture,
( ~ restaurant(skc7,X73)
| ~ in(skc7,X75,X73)
| ~ customer(skc7,X75)
| ~ ssSkC0
| nonreflexive(skc7,skf10(X74)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
cnf(clause27,negated_conjecture,
( ~ restaurant(skc7,X70)
| ~ in(skc7,X72,X70)
| ~ customer(skc7,X72)
| ~ ssSkC0
| past(skc7,skf10(X71)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
cnf(clause26,negated_conjecture,
( ~ restaurant(skc7,X67)
| ~ in(skc7,X69,X67)
| ~ customer(skc7,X69)
| ~ ssSkC0
| event(skc7,skf10(X68)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
cnf(clause25,negated_conjecture,
( ~ restaurant(skc7,X62)
| ~ in(skc7,X64,X62)
| ~ customer(skc7,X64)
| ~ ssSkC0
| event(skc7,skf9(X63)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
cnf(clause24,negated_conjecture,
( ~ restaurant(skc7,X51)
| ~ in(skc7,X53,X51)
| ~ customer(skc7,X53)
| ~ ssSkC0
| past(skc7,skf9(X52)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
cnf(clause10,negated_conjecture,
( ~ ssSkC0
| coffee(skc7,skc8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(clause1,negated_conjecture,
actual_world(skc18),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
cnf(clause7,negated_conjecture,
( ssSkC0
| coffee(skc18,skc23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
cnf(clause21,negated_conjecture,
( ~ coffee(X16,X17)
| ~ actual_world(X16)
| ssSkC0
| in(X16,skf25(X16,X17),skf21(X16,X17)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
cnf(c46,plain,
( ~ actual_world(skc18)
| ssSkC0
| in(skc18,skf25(skc18,skc23),skf21(skc18,skc23)) ),
inference(resolution,[status(thm)],[clause21,clause7]) ).
cnf(c52,plain,
( ssSkC0
| in(skc18,skf25(skc18,skc23),skf21(skc18,skc23)) ),
inference(resolution,[status(thm)],[c46,clause1]) ).
cnf(c53,plain,
( in(skc18,skf25(skc18,skc23),skf21(skc18,skc23))
| coffee(skc7,skc8) ),
inference(resolution,[status(thm)],[c52,clause10]) ).
cnf(clause23,negated_conjecture,
( ~ restaurant(skc7,X46)
| ~ in(skc7,X48,X46)
| ~ customer(skc7,X48)
| ~ ssSkC0
| nonreflexive(skc7,skf9(X47)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
cnf(clause22,negated_conjecture,
( ~ restaurant(skc7,X38)
| ~ in(skc7,X40,X38)
| ~ customer(skc7,X40)
| ~ ssSkC0
| see(skc7,skf9(X39)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
cnf(clause20,negated_conjecture,
( ~ in(skc18,X31,skc21)
| ~ customer(skc18,X31)
| ssSkC0
| patient(skc18,skf17(X32),skc20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
cnf(clause19,negated_conjecture,
( ~ in(skc18,X25,skc21)
| ~ customer(skc18,X25)
| ssSkC0
| agent(skc18,skf17(X25),X25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
cnf(clause18,negated_conjecture,
( ~ in(skc18,X22,skc21)
| ~ customer(skc18,X22)
| ssSkC0
| see(skc18,skf17(X23)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
cnf(clause17,negated_conjecture,
( ~ in(skc18,X20,skc21)
| ~ customer(skc18,X20)
| ssSkC0
| nonreflexive(skc18,skf17(X21)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
cnf(clause16,negated_conjecture,
( ~ in(skc18,X18,skc21)
| ~ customer(skc18,X18)
| ssSkC0
| past(skc18,skf17(X19)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(clause15,negated_conjecture,
( ~ in(skc18,X14,skc21)
| ~ customer(skc18,X14)
| ssSkC0
| event(skc18,skf17(X15)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
cnf(clause14,negated_conjecture,
( ~ coffee(X6,X8)
| ~ actual_world(X6)
| ssSkC0
| customer(X6,skf25(X6,X7)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
cnf(c26,plain,
( ~ actual_world(skc18)
| ssSkC0
| customer(skc18,skf25(skc18,X10)) ),
inference(resolution,[status(thm)],[clause14,clause7]) ).
cnf(c33,plain,
( ssSkC0
| customer(skc18,skf25(skc18,X11)) ),
inference(resolution,[status(thm)],[c26,clause1]) ).
cnf(c34,plain,
( customer(skc18,skf25(skc18,X13))
| coffee(skc7,skc8) ),
inference(resolution,[status(thm)],[c33,clause10]) ).
cnf(clause13,negated_conjecture,
( ~ coffee(X2,X4)
| ~ actual_world(X2)
| ssSkC0
| restaurant(X2,skf21(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
cnf(c10,plain,
( ~ actual_world(skc18)
| ssSkC0
| restaurant(skc18,skf21(skc18,X5)) ),
inference(resolution,[status(thm)],[clause13,clause7]) ).
cnf(c20,plain,
( ssSkC0
| restaurant(skc18,skf21(skc18,X9)) ),
inference(resolution,[status(thm)],[c10,clause1]) ).
cnf(c32,plain,
( restaurant(skc18,skf21(skc18,X12))
| coffee(skc7,skc8) ),
inference(resolution,[status(thm)],[c20,clause10]) ).
cnf(clause12,negated_conjecture,
( ssSkC0
| agent(skc18,skc19,skc20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
cnf(c8,plain,
( agent(skc18,skc19,skc20)
| coffee(skc7,skc8) ),
inference(resolution,[status(thm)],[clause12,clause10]) ).
cnf(clause11,negated_conjecture,
( ssSkC0
| patient(skc18,skc19,skc23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(c7,plain,
( patient(skc18,skc19,skc23)
| coffee(skc7,skc8) ),
inference(resolution,[status(thm)],[clause11,clause10]) ).
cnf(clause4,negated_conjecture,
( ssSkC0
| past(skc18,skc19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
cnf(c6,plain,
( coffee(skc7,skc8)
| past(skc18,skc19) ),
inference(resolution,[status(thm)],[clause10,clause4]) ).
cnf(c5,plain,
( coffee(skc7,skc8)
| coffee(skc18,skc23) ),
inference(resolution,[status(thm)],[clause10,clause7]) ).
cnf(clause3,negated_conjecture,
( ssSkC0
| event(skc18,skc19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(c4,plain,
( coffee(skc7,skc8)
| event(skc18,skc19) ),
inference(resolution,[status(thm)],[clause10,clause3]) ).
cnf(clause5,negated_conjecture,
( ssSkC0
| nonreflexive(skc18,skc19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
cnf(c3,plain,
( coffee(skc7,skc8)
| nonreflexive(skc18,skc19) ),
inference(resolution,[status(thm)],[clause10,clause5]) ).
cnf(clause8,negated_conjecture,
( ssSkC0
| human_person(skc18,skc20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
cnf(c2,plain,
( coffee(skc7,skc8)
| human_person(skc18,skc20) ),
inference(resolution,[status(thm)],[clause10,clause8]) ).
cnf(clause9,negated_conjecture,
( ssSkC0
| restaurant(skc18,skc21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
cnf(c1,plain,
( coffee(skc7,skc8)
| restaurant(skc18,skc21) ),
inference(resolution,[status(thm)],[clause10,clause9]) ).
cnf(clause6,negated_conjecture,
( ssSkC0
| drink(skc18,skc19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
cnf(c0,plain,
( coffee(skc7,skc8)
| drink(skc18,skc19) ),
inference(resolution,[status(thm)],[clause10,clause6]) ).
cnf(clause2,negated_conjecture,
actual_world(skc7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : NLP102-1 : TPTP v8.1.2. Released v2.4.0.
% 0.11/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n026.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed May 8 13:24:53 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.43/0.60 % Version: 1.5
% 0.43/0.60 % SZS status Satisfiable
% 0.43/0.60 % SZS output start Saturation
% See solution above
% 0.43/0.60
% 0.43/0.60 % Initial clauses : 38
% 0.43/0.60 % Processed clauses : 57
% 0.43/0.60 % Factors computed : 1
% 0.43/0.60 % Resolvents computed: 61
% 0.43/0.60 % Tautologies deleted: 2
% 0.43/0.60 % Forward subsumed : 41
% 0.43/0.60 % Backward subsumed : 3
% 0.43/0.60 % -------- CPU Time ---------
% 0.43/0.60 % User time : 0.240 s
% 0.43/0.60 % System time : 0.015 s
% 0.43/0.60 % Total time : 0.255 s
%------------------------------------------------------------------------------