%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PUZ005-1 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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:37:33 EDT 2024
% Result : Unsatisfiable 1.36s 1.58s
% Output : Refutation 1.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 22
% Syntax : Number of clauses : 54 ( 16 unt; 21 nHn; 54 RR)
% Number of literals : 111 ( 0 equ; 37 neg)
% Maximal clause size : 4 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 10 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-1 aty)
% Number of variables : 24 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(wednesday_not_saturday,axiom,
( ~ wednesday(X16)
| ~ saturday(X16) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wednesday_not_saturday) ).
cnf(yesterday_saturday,axiom,
( saturday(yesterday(X36))
| ~ sunday(X36) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',yesterday_saturday) ).
cnf(admissions6,axiom,
admits(unicorn,today,yesterday(today)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',admissions6) ).
cnf(admissions3,axiom,
( ~ member(X53,lying_days(X54))
| ~ admits(X54,X53,X52)
| ~ member(X52,lying_days(X54)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',admissions3) ).
cnf(unicorn_lies_on_friday,axiom,
( ~ friday(X43)
| member(X43,lying_days(unicorn)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unicorn_lies_on_friday) ).
cnf(yesterday_friday,axiom,
( friday(yesterday(X35))
| ~ saturday(X35) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',yesterday_friday) ).
cnf(unicorn_lies_on_thursday,axiom,
( ~ thursday(X41)
| member(X41,lying_days(unicorn)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unicorn_lies_on_thursday) ).
cnf(yesterday_thursday,axiom,
( thursday(yesterday(X34))
| ~ friday(X34) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',yesterday_thursday) ).
cnf(prove_today_is_thursday,negated_conjecture,
~ thursday(today),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_today_is_thursday) ).
cnf(unicorns_lying_days,axiom,
( ~ member(X45,lying_days(unicorn))
| thursday(X45)
| friday(X45)
| saturday(X45) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unicorns_lying_days) ).
cnf(admissions1,axiom,
( member(X47,lying_days(X48))
| ~ admits(X48,X47,X46)
| member(X46,lying_days(X48)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',admissions1) ).
cnf(c42,plain,
( member(today,lying_days(unicorn))
| member(yesterday(today),lying_days(unicorn)) ),
inference(resolution,[status(thm)],[admissions1,admissions6]) ).
cnf(c47,plain,
( member(yesterday(today),lying_days(unicorn))
| thursday(today)
| friday(today)
| saturday(today) ),
inference(resolution,[status(thm)],[c42,unicorns_lying_days]) ).
cnf(c95,plain,
( member(yesterday(today),lying_days(unicorn))
| friday(today)
| saturday(today) ),
inference(resolution,[status(thm)],[c47,prove_today_is_thursday]) ).
cnf(c162,plain,
( member(yesterday(today),lying_days(unicorn))
| saturday(today)
| thursday(yesterday(today)) ),
inference(resolution,[status(thm)],[c95,yesterday_thursday]) ).
cnf(c286,plain,
( member(yesterday(today),lying_days(unicorn))
| saturday(today) ),
inference(resolution,[status(thm)],[c162,unicorn_lies_on_thursday]) ).
cnf(c297,plain,
( member(yesterday(today),lying_days(unicorn))
| friday(yesterday(today)) ),
inference(resolution,[status(thm)],[c286,yesterday_friday]) ).
cnf(c360,plain,
member(yesterday(today),lying_days(unicorn)),
inference(resolution,[status(thm)],[c297,unicorn_lies_on_friday]) ).
cnf(c365,plain,
( ~ member(X86,lying_days(unicorn))
| ~ admits(unicorn,X86,yesterday(today)) ),
inference(resolution,[status(thm)],[c360,admissions3]) ).
cnf(c411,plain,
~ member(today,lying_days(unicorn)),
inference(resolution,[status(thm)],[c365,admissions6]) ).
cnf(unicorn_lies_on_saturday,axiom,
( ~ saturday(X44)
| member(X44,lying_days(unicorn)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unicorn_lies_on_saturday) ).
cnf(saturday_yesterday,axiom,
( ~ saturday(yesterday(X29))
| sunday(X29) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',saturday_yesterday) ).
cnf(thursday_yesterday,axiom,
( ~ thursday(yesterday(X27))
| friday(X27) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thursday_yesterday) ).
cnf(friday_yesterday,axiom,
( ~ friday(yesterday(X28))
| saturday(X28) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',friday_yesterday) ).
cnf(c356,plain,
( friday(yesterday(today))
| thursday(yesterday(today))
| saturday(yesterday(today)) ),
inference(resolution,[status(thm)],[c297,unicorns_lying_days]) ).
cnf(c553,plain,
( thursday(yesterday(today))
| saturday(yesterday(today))
| saturday(today) ),
inference(resolution,[status(thm)],[c356,friday_yesterday]) ).
cnf(c569,plain,
( saturday(yesterday(today))
| saturday(today)
| friday(today) ),
inference(resolution,[status(thm)],[c553,thursday_yesterday]) ).
cnf(c593,plain,
( saturday(today)
| friday(today)
| sunday(today) ),
inference(resolution,[status(thm)],[c569,saturday_yesterday]) ).
cnf(c610,plain,
( friday(today)
| sunday(today)
| member(today,lying_days(unicorn)) ),
inference(resolution,[status(thm)],[c593,unicorn_lies_on_saturday]) ).
cnf(c1920,plain,
( sunday(today)
| member(today,lying_days(unicorn)) ),
inference(resolution,[status(thm)],[c610,unicorn_lies_on_friday]) ).
cnf(c2407,plain,
sunday(today),
inference(resolution,[status(thm)],[c1920,c411]) ).
cnf(c2411,plain,
saturday(yesterday(today)),
inference(resolution,[status(thm)],[c2407,yesterday_saturday]) ).
cnf(c2509,plain,
~ wednesday(yesterday(today)),
inference(resolution,[status(thm)],[c2411,wednesday_not_saturday]) ).
cnf(tuesday_not_saturday,axiom,
( ~ tuesday(X12)
| ~ saturday(X12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tuesday_not_saturday) ).
cnf(c2505,plain,
~ tuesday(yesterday(today)),
inference(resolution,[status(thm)],[c2411,tuesday_not_saturday]) ).
cnf(monday_not_saturday,axiom,
( ~ monday(X7)
| ~ saturday(X7) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',monday_not_saturday) ).
cnf(c2508,plain,
~ monday(yesterday(today)),
inference(resolution,[status(thm)],[c2411,monday_not_saturday]) ).
cnf(lions_lying_days,axiom,
( ~ member(X42,lying_days(lion))
| monday(X42)
| tuesday(X42)
| wednesday(X42) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lions_lying_days) ).
cnf(tuesday_not_sunday,axiom,
( ~ tuesday(X13)
| ~ sunday(X13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tuesday_not_sunday) ).
cnf(c2416,plain,
~ tuesday(today),
inference(resolution,[status(thm)],[c2407,tuesday_not_sunday]) ).
cnf(monday_not_sunday,axiom,
( ~ monday(X8)
| ~ sunday(X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',monday_not_sunday) ).
cnf(c2414,plain,
~ monday(today),
inference(resolution,[status(thm)],[c2407,monday_not_sunday]) ).
cnf(admissions5,axiom,
admits(lion,today,yesterday(today)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',admissions5) ).
cnf(c43,plain,
( member(today,lying_days(lion))
| member(yesterday(today),lying_days(lion)) ),
inference(resolution,[status(thm)],[admissions1,admissions5]) ).
cnf(c53,plain,
( member(yesterday(today),lying_days(lion))
| monday(today)
| tuesday(today)
| wednesday(today) ),
inference(resolution,[status(thm)],[c43,lions_lying_days]) ).
cnf(wednesday_not_sunday,axiom,
( ~ wednesday(X17)
| ~ sunday(X17) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wednesday_not_sunday) ).
cnf(c2413,plain,
~ wednesday(today),
inference(resolution,[status(thm)],[c2407,wednesday_not_sunday]) ).
cnf(c2443,plain,
( member(yesterday(today),lying_days(lion))
| monday(today)
| tuesday(today) ),
inference(resolution,[status(thm)],[c2413,c53]) ).
cnf(c2927,plain,
( member(yesterday(today),lying_days(lion))
| tuesday(today) ),
inference(resolution,[status(thm)],[c2443,c2414]) ).
cnf(c2941,plain,
member(yesterday(today),lying_days(lion)),
inference(resolution,[status(thm)],[c2927,c2416]) ).
cnf(c2942,plain,
( monday(yesterday(today))
| tuesday(yesterday(today))
| wednesday(yesterday(today)) ),
inference(resolution,[status(thm)],[c2941,lions_lying_days]) ).
cnf(c3407,plain,
( tuesday(yesterday(today))
| wednesday(yesterday(today)) ),
inference(resolution,[status(thm)],[c2942,c2508]) ).
cnf(c3447,plain,
wednesday(yesterday(today)),
inference(resolution,[status(thm)],[c3407,c2505]) ).
cnf(c3471,plain,
$false,
inference(resolution,[status(thm)],[c3447,c2509]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : PUZ005-1 : TPTP v8.1.2. Released v1.0.0.
% 0.10/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n013.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 20:39:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 1.36/1.58 % Version: 1.5
% 1.36/1.58 % SZS status Unsatisfiable
% 1.36/1.58 % SZS output start CNFRefutation
% See solution above
% 1.36/1.58
% 1.36/1.58 % Initial clauses : 51
% 1.36/1.58 % Processed clauses : 252
% 1.36/1.58 % Factors computed : 5
% 1.36/1.58 % Resolvents computed: 3467
% 1.36/1.58 % Tautologies deleted: 64
% 1.36/1.58 % Forward subsumed : 231
% 1.36/1.58 % Backward subsumed : 110
% 1.36/1.58 % -------- CPU Time ---------
% 1.36/1.58 % User time : 1.217 s
% 1.36/1.58 % System time : 0.020 s
% 1.36/1.58 % Total time : 1.237 s
%------------------------------------------------------------------------------