%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PUZ005+1 : TPTP v8.1.2. Released v2.2.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 : Theorem 3.39s 3.55s
% Output : Refutation 3.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : PUZ005+1 : TPTP v8.1.2. Released v2.2.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n013.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed May 8 20:38:38 EDT 2024
% 0.14/0.34 % CPUTime :
% 3.39/3.55 % Version: 1.5
% 3.39/3.55 % SZS status Theorem
% 3.39/3.55 % SZS output start CNFRefutation
% 3.39/3.55 fof(unicorn_lies_on_a_day,axiom,(![X]:(unicorn_lies(X)=>day(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', unicorn_lies_on_a_day)).
% 3.39/3.55 fof(c44,plain,(![X]:(~unicorn_lies(X)|day(X))),inference(fof_nnf,[status(thm)],[unicorn_lies_on_a_day])).
% 3.39/3.55 fof(c45,plain,(![X19]:(~unicorn_lies(X19)|day(X19))),inference(variable_rename,[status(thm)],[c44])).
% 3.39/3.55 cnf(c46,plain,~unicorn_lies(X50)|day(X50),inference(split_conjunct,[status(thm)],[c45])).
% 3.39/3.55 fof(thursday,axiom,thursday(a_thursday),file('/export/starexec/sandbox/benchmark/theBenchmark.p', thursday)).
% 3.39/3.55 cnf(c145,plain,thursday(a_thursday),inference(split_conjunct,[status(thm)],[thursday])).
% 3.39/3.55 fof(unicorn_lies_thursday,axiom,(![X]:(thursday(X)=>unicorn_lies(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', unicorn_lies_thursday)).
% 3.39/3.55 fof(c60,plain,(![X]:(~thursday(X)|unicorn_lies(X))),inference(fof_nnf,[status(thm)],[unicorn_lies_thursday])).
% 3.39/3.55 fof(c61,plain,(![X24]:(~thursday(X24)|unicorn_lies(X24))),inference(variable_rename,[status(thm)],[c60])).
% 3.39/3.55 cnf(c62,plain,~thursday(X59)|unicorn_lies(X59),inference(split_conjunct,[status(thm)],[c61])).
% 3.39/3.55 cnf(c159,plain,unicorn_lies(a_thursday),inference(resolution,[status(thm)],[c62, c145])).
% 3.39/3.55 cnf(c163,plain,day(a_thursday),inference(resolution,[status(thm)],[c159, c46])).
% 3.39/3.55 fof(lion_does_not_lie_thursday,axiom,(![X]:(thursday(X)=>(~lion_lies(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', lion_does_not_lie_thursday)).
% 3.39/3.55 fof(c87,plain,(![X]:(thursday(X)=>~lion_lies(X))),inference(fof_simplification,[status(thm)],[lion_does_not_lie_thursday])).
% 3.39/3.55 fof(c88,plain,(![X]:(~thursday(X)|~lion_lies(X))),inference(fof_nnf,[status(thm)],[c87])).
% 3.39/3.55 fof(c89,plain,(![X31]:(~thursday(X31)|~lion_lies(X31))),inference(variable_rename,[status(thm)],[c88])).
% 3.39/3.55 cnf(c90,plain,~thursday(X74)|~lion_lies(X74),inference(split_conjunct,[status(thm)],[c89])).
% 3.39/3.55 fof(wednesday_is_a_day,axiom,(![X]:(wednesday(X)=>day(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', wednesday_is_a_day)).
% 3.39/3.55 fof(c133,plain,(![X]:(~wednesday(X)|day(X))),inference(fof_nnf,[status(thm)],[wednesday_is_a_day])).
% 3.39/3.55 fof(c134,plain,(![X46]:(~wednesday(X46)|day(X46))),inference(variable_rename,[status(thm)],[c133])).
% 3.39/3.55 cnf(c135,plain,~wednesday(X89)|day(X89),inference(split_conjunct,[status(thm)],[c134])).
% 3.39/3.55 fof(thursday_follows_wednesday,axiom,(![X]:(thursday(X)=>wednesday(yesterday(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', thursday_follows_wednesday)).
% 3.39/3.55 fof(c109,plain,(![X]:(~thursday(X)|wednesday(yesterday(X)))),inference(fof_nnf,[status(thm)],[thursday_follows_wednesday])).
% 3.39/3.55 fof(c110,plain,(![X38]:(~thursday(X38)|wednesday(yesterday(X38)))),inference(variable_rename,[status(thm)],[c109])).
% 3.39/3.55 cnf(c111,plain,~thursday(X91)|wednesday(yesterday(X91)),inference(split_conjunct,[status(thm)],[c110])).
% 3.39/3.55 cnf(c206,plain,wednesday(yesterday(a_thursday)),inference(resolution,[status(thm)],[c111, c145])).
% 3.39/3.55 cnf(c219,plain,day(yesterday(a_thursday)),inference(resolution,[status(thm)],[c206, c135])).
% 3.39/3.55 fof(lion_lies_on_neither,axiom,(![X]:(day(X)=>(![Y]:(day(Y)=>(((~lion_lies(X))&(~lies_on_one_of(a_lion,X,Y)))=>(~lion_lies(Y))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', lion_lies_on_neither)).
% 3.39/3.55 fof(c29,plain,(![X]:(day(X)=>(![Y]:(day(Y)=>((~lion_lies(X)&~lies_on_one_of(a_lion,X,Y))=>~lion_lies(Y)))))),inference(fof_simplification,[status(thm)],[lion_lies_on_neither])).
% 3.39/3.55 fof(c30,plain,(![X]:(~day(X)|(![Y]:(~day(Y)|((lion_lies(X)|lies_on_one_of(a_lion,X,Y))|~lion_lies(Y)))))),inference(fof_nnf,[status(thm)],[c29])).
% 3.39/3.55 fof(c32,plain,(![X13]:(![X14]:(~day(X13)|(~day(X14)|((lion_lies(X13)|lies_on_one_of(a_lion,X13,X14))|~lion_lies(X14)))))),inference(shift_quantors,[status(thm)],[fof(c31,plain,(![X13]:(~day(X13)|(![X14]:(~day(X14)|((lion_lies(X13)|lies_on_one_of(a_lion,X13,X14))|~lion_lies(X14)))))),inference(variable_rename,[status(thm)],[c30])).])).
% 3.39/3.55 cnf(c33,plain,~day(X71)|~day(X70)|lion_lies(X71)|lies_on_one_of(a_lion,X71,X70)|~lion_lies(X70),inference(split_conjunct,[status(thm)],[c32])).
% 3.39/3.55 fof(lion_lies_wednesday,axiom,(![X]:(wednesday(X)=>lion_lies(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', lion_lies_wednesday)).
% 3.39/3.55 fof(c91,plain,(![X]:(~wednesday(X)|lion_lies(X))),inference(fof_nnf,[status(thm)],[lion_lies_wednesday])).
% 3.39/3.55 fof(c92,plain,(![X32]:(~wednesday(X32)|lion_lies(X32))),inference(variable_rename,[status(thm)],[c91])).
% 3.39/3.55 cnf(c93,plain,~wednesday(X75)|lion_lies(X75),inference(split_conjunct,[status(thm)],[c92])).
% 3.39/3.55 cnf(c220,plain,lion_lies(yesterday(a_thursday)),inference(resolution,[status(thm)],[c206, c93])).
% 3.39/3.55 cnf(c248,plain,~day(X115)|~day(yesterday(a_thursday))|lion_lies(X115)|lies_on_one_of(a_lion,X115,yesterday(a_thursday)),inference(resolution,[status(thm)],[c220, c33])).
% 3.39/3.55 cnf(c553,plain,~day(X143)|lion_lies(X143)|lies_on_one_of(a_lion,X143,yesterday(a_thursday)),inference(resolution,[status(thm)],[c248, c219])).
% 3.39/3.55 cnf(c2367,plain,lion_lies(a_thursday)|lies_on_one_of(a_lion,a_thursday,yesterday(a_thursday)),inference(resolution,[status(thm)],[c553, c163])).
% 3.39/3.55 cnf(c2403,plain,lies_on_one_of(a_lion,a_thursday,yesterday(a_thursday))|~thursday(a_thursday),inference(resolution,[status(thm)],[c2367, c90])).
% 3.39/3.55 cnf(c2430,plain,lies_on_one_of(a_lion,a_thursday,yesterday(a_thursday)),inference(resolution,[status(thm)],[c2403, c145])).
% 3.39/3.55 fof(prove_there_are_close_lying_days,conjecture,(?[X]:((day(X)&lies_on_one_of(a_lion,X,yesterday(X)))&lies_on_one_of(a_unicorn,X,yesterday(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_there_are_close_lying_days)).
% 3.39/3.55 fof(c0,negated_conjecture,(~(?[X]:((day(X)&lies_on_one_of(a_lion,X,yesterday(X)))&lies_on_one_of(a_unicorn,X,yesterday(X))))),inference(assume_negation,[status(cth)],[prove_there_are_close_lying_days])).
% 3.39/3.55 fof(c1,negated_conjecture,(![X]:((~day(X)|~lies_on_one_of(a_lion,X,yesterday(X)))|~lies_on_one_of(a_unicorn,X,yesterday(X)))),inference(fof_nnf,[status(thm)],[c0])).
% 3.39/3.55 fof(c2,negated_conjecture,(![X2]:((~day(X2)|~lies_on_one_of(a_lion,X2,yesterday(X2)))|~lies_on_one_of(a_unicorn,X2,yesterday(X2)))),inference(variable_rename,[status(thm)],[c1])).
% 3.39/3.55 cnf(c3,negated_conjecture,~day(X49)|~lies_on_one_of(a_lion,X49,yesterday(X49))|~lies_on_one_of(a_unicorn,X49,yesterday(X49)),inference(split_conjunct,[status(thm)],[c2])).
% 3.39/3.55 fof(unicorn_does_not_lie_wednesday,axiom,(![X]:(wednesday(X)=>(~unicorn_lies(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', unicorn_does_not_lie_wednesday)).
% 3.39/3.55 fof(c63,plain,(![X]:(wednesday(X)=>~unicorn_lies(X))),inference(fof_simplification,[status(thm)],[unicorn_does_not_lie_wednesday])).
% 3.39/3.55 fof(c64,plain,(![X]:(~wednesday(X)|~unicorn_lies(X))),inference(fof_nnf,[status(thm)],[c63])).
% 3.39/3.55 fof(c65,plain,(![X25]:(~wednesday(X25)|~unicorn_lies(X25))),inference(variable_rename,[status(thm)],[c64])).
% 3.39/3.55 cnf(c66,plain,~wednesday(X62)|~unicorn_lies(X62),inference(split_conjunct,[status(thm)],[c65])).
% 3.39/3.55 fof(unicorn_lies_on_both,axiom,(![X]:(day(X)=>(![Y]:(day(Y)=>((unicorn_lies(X)&(~lies_on_one_of(a_unicorn,X,Y)))=>unicorn_lies(Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', unicorn_lies_on_both)).
% 3.39/3.55 fof(c4,plain,(![X]:(day(X)=>(![Y]:(day(Y)=>((unicorn_lies(X)&~lies_on_one_of(a_unicorn,X,Y))=>unicorn_lies(Y)))))),inference(fof_simplification,[status(thm)],[unicorn_lies_on_both])).
% 3.39/3.55 fof(c5,plain,(![X]:(~day(X)|(![Y]:(~day(Y)|((~unicorn_lies(X)|lies_on_one_of(a_unicorn,X,Y))|unicorn_lies(Y)))))),inference(fof_nnf,[status(thm)],[c4])).
% 3.39/3.55 fof(c7,plain,(![X3]:(![X4]:(~day(X3)|(~day(X4)|((~unicorn_lies(X3)|lies_on_one_of(a_unicorn,X3,X4))|unicorn_lies(X4)))))),inference(shift_quantors,[status(thm)],[fof(c6,plain,(![X3]:(~day(X3)|(![X4]:(~day(X4)|((~unicorn_lies(X3)|lies_on_one_of(a_unicorn,X3,X4))|unicorn_lies(X4)))))),inference(variable_rename,[status(thm)],[c5])).])).
% 3.39/3.55 cnf(c8,plain,~day(X54)|~day(X53)|~unicorn_lies(X54)|lies_on_one_of(a_unicorn,X54,X53)|unicorn_lies(X53),inference(split_conjunct,[status(thm)],[c7])).
% 3.39/3.55 cnf(c162,plain,~day(a_thursday)|~day(X101)|lies_on_one_of(a_unicorn,a_thursday,X101)|unicorn_lies(X101),inference(resolution,[status(thm)],[c159, c8])).
% 3.39/3.55 cnf(c312,plain,~day(a_thursday)|lies_on_one_of(a_unicorn,a_thursday,yesterday(a_thursday))|unicorn_lies(yesterday(a_thursday)),inference(resolution,[status(thm)],[c162, c219])).
% 3.39/3.55 cnf(c1062,plain,lies_on_one_of(a_unicorn,a_thursday,yesterday(a_thursday))|unicorn_lies(yesterday(a_thursday)),inference(resolution,[status(thm)],[c312, c163])).
% 3.39/3.55 cnf(c3017,plain,lies_on_one_of(a_unicorn,a_thursday,yesterday(a_thursday))|~wednesday(yesterday(a_thursday)),inference(resolution,[status(thm)],[c1062, c66])).
% 3.39/3.55 cnf(c3415,plain,lies_on_one_of(a_unicorn,a_thursday,yesterday(a_thursday)),inference(resolution,[status(thm)],[c3017, c206])).
% 3.39/3.55 cnf(c3419,plain,~day(a_thursday)|~lies_on_one_of(a_lion,a_thursday,yesterday(a_thursday)),inference(resolution,[status(thm)],[c3415, c3])).
% 3.39/3.55 cnf(c3420,plain,~day(a_thursday),inference(resolution,[status(thm)],[c3419, c2430])).
% 3.39/3.55 cnf(c3421,plain,$false,inference(resolution,[status(thm)],[c3420, c163])).
% 3.39/3.55 % SZS output end CNFRefutation
% 3.39/3.55
% 3.39/3.55 % Initial clauses : 46
% 3.39/3.55 % Processed clauses : 1033
% 3.39/3.55 % Factors computed : 54
% 3.39/3.55 % Resolvents computed: 3219
% 3.39/3.55 % Tautologies deleted: 2
% 3.39/3.55 % Forward subsumed : 660
% 3.39/3.55 % Backward subsumed : 462
% 3.39/3.55 % -------- CPU Time ---------
% 3.39/3.55 % User time : 3.184 s
% 3.39/3.55 % System time : 0.024 s
% 3.39/3.55 % Total time : 3.208 s
%------------------------------------------------------------------------------