%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : PUZ005+1 : TPTP v8.1.0. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n032.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 : 600s
% DateTime : Mon Jul 18 18:19:03 EDT 2022
% Result : Theorem 9.27s 9.62s
% Output : Proof 9.27s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.10 % Problem : PUZ005+1 : TPTP v8.1.0. Released v2.2.0.
% 0.03/0.11 % Command : leancop_casc.sh %s %d
% 0.11/0.30 % Computer : n032.cluster.edu
% 0.11/0.30 % Model : x86_64 x86_64
% 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.30 % Memory : 8042.1875MB
% 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.30 % CPULimit : 300
% 0.11/0.30 % WCLimit : 600
% 0.11/0.30 % DateTime : Sat May 28 22:00:26 EDT 2022
% 0.11/0.30 % CPUTime :
% 9.27/9.62 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.27/9.63 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.27/9.63
% 9.27/9.63 %-----------------------------------------------------
% 9.27/9.63 fof(prove_there_are_close_lying_days, conjecture, ? [_34879] : (day(_34879) & lies_on_one_of(a_lion, _34879, yesterday(_34879)) & lies_on_one_of(a_unicorn, _34879, yesterday(_34879))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_there_are_close_lying_days)).
% 9.27/9.63 fof(thursday, axiom, thursday(a_thursday), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', thursday)).
% 9.27/9.63 fof(wednesday_is_a_day, axiom, ! [_35122] : (wednesday(_35122) => day(_35122)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', wednesday_is_a_day)).
% 9.27/9.63 fof(thursday_is_a_day, axiom, ! [_35243] : (thursday(_35243) => day(_35243)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', thursday_is_a_day)).
% 9.27/9.63 fof(thursday_follows_wednesday, axiom, ! [_35370] : (thursday(_35370) => wednesday(yesterday(_35370))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', thursday_follows_wednesday)).
% 9.27/9.63 fof(lion_lies_wednesday, axiom, ! [_35505] : (wednesday(_35505) => lion_lies(_35505)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', lion_lies_wednesday)).
% 9.27/9.63 fof(lion_does_not_lie_thursday, axiom, ! [_35626] : (thursday(_35626) => ~ lion_lies(_35626)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', lion_does_not_lie_thursday)).
% 9.27/9.63 fof(unicorn_does_not_lie_wednesday, axiom, ! [_35759] : (wednesday(_35759) => ~ unicorn_lies(_35759)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', unicorn_does_not_lie_wednesday)).
% 9.27/9.63 fof(unicorn_lies_thursday, axiom, ! [_35887] : (thursday(_35887) => unicorn_lies(_35887)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', unicorn_lies_thursday)).
% 9.27/9.63 fof(lion_lies_on_neither, axiom, ! [_36015] : (day(_36015) => ! [_36030] : (day(_36030) => ~ lion_lies(_36015) & ~ lies_on_one_of(a_lion, _36015, _36030) => ~ lion_lies(_36030))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', lion_lies_on_neither)).
% 9.27/9.63 fof(unicorn_lies_on_both, axiom, ! [_36268] : (day(_36268) => ! [_36283] : (day(_36283) => unicorn_lies(_36268) & ~ lies_on_one_of(a_unicorn, _36268, _36283) => unicorn_lies(_36283))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', unicorn_lies_on_both)).
% 9.27/9.63
% 9.27/9.63 cnf(1, plain, [day(_22352), lies_on_one_of(a_lion, _22352, yesterday(_22352)), lies_on_one_of(a_unicorn, _22352, yesterday(_22352))], clausify(prove_there_are_close_lying_days)).
% 9.27/9.63 cnf(2, plain, [-(thursday(a_thursday))], clausify(thursday)).
% 9.27/9.63 cnf(3, plain, [wednesday(_11217), -(day(_11217))], clausify(wednesday_is_a_day)).
% 9.27/9.63 cnf(4, plain, [thursday(_11427), -(day(_11427))], clausify(thursday_is_a_day)).
% 9.27/9.63 cnf(5, plain, [thursday(_12951), -(wednesday(yesterday(_12951)))], clausify(thursday_follows_wednesday)).
% 9.27/9.63 cnf(6, plain, [wednesday(_14283), -(lion_lies(_14283))], clausify(lion_lies_wednesday)).
% 9.27/9.63 cnf(7, plain, [thursday(_14493), lion_lies(_14493)], clausify(lion_does_not_lie_thursday)).
% 9.27/9.63 cnf(8, plain, [wednesday(_15861), unicorn_lies(_15861)], clausify(unicorn_does_not_lie_wednesday)).
% 9.27/9.63 cnf(9, plain, [thursday(_16089), -(unicorn_lies(_16089))], clausify(unicorn_lies_thursday)).
% 9.27/9.63 cnf(10, plain, [day(_18433), day(_18537), lion_lies(_18537), -(lion_lies(_18433)), -(lies_on_one_of(a_lion, _18433, _18537))], clausify(lion_lies_on_neither)).
% 9.27/9.63 cnf(11, plain, [day(_21168), day(_21268), -(unicorn_lies(_21268)), unicorn_lies(_21168), -(lies_on_one_of(a_unicorn, _21168, _21268))], clausify(unicorn_lies_on_both)).
% 9.27/9.63
% 9.27/9.63 cnf('1',plain,[day(a_thursday), lies_on_one_of(a_lion, a_thursday, yesterday(a_thursday)), lies_on_one_of(a_unicorn, a_thursday, yesterday(a_thursday))],start(1,bind([[_22352], [a_thursday]]))).
% 9.27/9.63 cnf('1.1',plain,[-(day(a_thursday)), thursday(a_thursday)],extension(4,bind([[_11427], [a_thursday]]))).
% 9.27/9.63 cnf('1.1.1',plain,[-(thursday(a_thursday))],extension(2)).
% 9.27/9.63 cnf('1.2',plain,[-(lies_on_one_of(a_lion, a_thursday, yesterday(a_thursday))), day(a_thursday), day(yesterday(a_thursday)), lion_lies(yesterday(a_thursday)), -(lion_lies(a_thursday))],extension(10,bind([[_18537, _18433], [yesterday(a_thursday), a_thursday]]))).
% 9.27/9.63 cnf('1.2.1',plain,[-(day(a_thursday))],lemmata('1')).
% 9.27/9.63 cnf('1.2.2',plain,[-(day(yesterday(a_thursday))), wednesday(yesterday(a_thursday))],extension(3,bind([[_11217], [yesterday(a_thursday)]]))).
% 9.27/9.63 cnf('1.2.2.1',plain,[-(wednesday(yesterday(a_thursday))), thursday(a_thursday)],extension(5,bind([[_12951], [a_thursday]]))).
% 9.27/9.63 cnf('1.2.2.1.1',plain,[-(thursday(a_thursday))],extension(2)).
% 9.27/9.63 cnf('1.2.3',plain,[-(lion_lies(yesterday(a_thursday))), wednesday(yesterday(a_thursday))],extension(6,bind([[_14283], [yesterday(a_thursday)]]))).
% 9.27/9.63 cnf('1.2.3.1',plain,[-(wednesday(yesterday(a_thursday))), thursday(a_thursday)],extension(5,bind([[_12951], [a_thursday]]))).
% 9.27/9.63 cnf('1.2.3.1.1',plain,[-(thursday(a_thursday))],extension(2)).
% 9.27/9.63 cnf('1.2.4',plain,[lion_lies(a_thursday), thursday(a_thursday)],extension(7,bind([[_14493], [a_thursday]]))).
% 9.27/9.63 cnf('1.2.4.1',plain,[-(thursday(a_thursday))],extension(2)).
% 9.27/9.63 cnf('1.3',plain,[-(lies_on_one_of(a_unicorn, a_thursday, yesterday(a_thursday))), day(a_thursday), day(yesterday(a_thursday)), -(unicorn_lies(yesterday(a_thursday))), unicorn_lies(a_thursday)],extension(11,bind([[_21268, _21168], [yesterday(a_thursday), a_thursday]]))).
% 9.27/9.63 cnf('1.3.1',plain,[-(day(a_thursday))],lemmata('1')).
% 9.27/9.63 cnf('1.3.2',plain,[-(day(yesterday(a_thursday))), wednesday(yesterday(a_thursday))],extension(3,bind([[_11217], [yesterday(a_thursday)]]))).
% 9.27/9.63 cnf('1.3.2.1',plain,[-(wednesday(yesterday(a_thursday))), thursday(a_thursday)],extension(5,bind([[_12951], [a_thursday]]))).
% 9.27/9.63 cnf('1.3.2.1.1',plain,[-(thursday(a_thursday))],extension(2)).
% 9.27/9.63 cnf('1.3.3',plain,[unicorn_lies(yesterday(a_thursday)), wednesday(yesterday(a_thursday))],extension(8,bind([[_15861], [yesterday(a_thursday)]]))).
% 9.27/9.63 cnf('1.3.3.1',plain,[-(wednesday(yesterday(a_thursday))), thursday(a_thursday)],extension(5,bind([[_12951], [a_thursday]]))).
% 9.27/9.63 cnf('1.3.3.1.1',plain,[-(thursday(a_thursday))],extension(2)).
% 9.27/9.63 cnf('1.3.4',plain,[-(unicorn_lies(a_thursday)), thursday(a_thursday)],extension(9,bind([[_16089], [a_thursday]]))).
% 9.27/9.63 cnf('1.3.4.1',plain,[-(thursday(a_thursday))],extension(2)).
% 9.27/9.63 %-----------------------------------------------------
% 9.27/9.64
% 9.27/9.64 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------