%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : PUZ018-1 : TPTP v9.3.1. Bugfixed v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:31:52 PM UTC 2026
% Result : Unsatisfiable 218.37s 74.55s
% Output : Proof 218.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 25
% Syntax : Number of formulae : 157 ( 74 unt; 0 def)
% Number of atoms : 470 ( 0 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 454 ( 141 ~; 313 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 10 con; 0-0 aty)
% Number of variables : 81 ( 8 sgn 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f40,hypothesis,
( same_day(Y,Z)
| same_person(X,W)
| on(W,Z)
| on(W,Y)
| on(X,Z)
| on(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',no_two_off_twice_together) ).
fof(f40_nnf,plain,
! [X,Y,Z,W] :
( same_day(Y,Z)
| same_person(X,W)
| on(W,Z)
| on(W,Y)
| on(X,Z)
| on(X,Y) ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [X,Y,Z,W] :
( same_day(Y,Z)
| same_person(X,W)
| on(W,Z)
| on(W,Y)
| on(X,Z)
| on(X,Y) ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c40,plain,
( same_day(X1,X2)
| same_person(X0,X3)
| on(X3,X2)
| on(X3,X1)
| on(X0,X2)
| on(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(f14,axiom,
~ same_person(a,c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_not_c) ).
fof(f14_nnf,plain,
~ same_person(a,c),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
~ same_person(a,c),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
~ same_person(a,c),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p69,plain,
( same_day(X0,X1)
| on(c,X1)
| on(c,X0)
| on(a,X1)
| on(a,X0) ),
inference(resolution,[status(thm)],[c40,c14]) ).
cnf(f20,axiom,
~ same_day(sunday,thursday),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sunday_not_thursday) ).
fof(f20_nnf,plain,
~ same_day(sunday,thursday),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
~ same_day(sunday,thursday),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
~ same_day(sunday,thursday),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p249,plain,
( on(c,thursday)
| on(c,sunday)
| on(a,thursday)
| on(a,sunday) ),
inference(resolution,[status(thm)],[p69,c20]) ).
cnf(f39,hypothesis,
( ~ on(U,Z)
| ~ on(U,Y)
| ~ on(U,X)
| ~ consecutive(Z,W)
| ~ consecutive(Y,Z)
| ~ consecutive(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_on_for_3_days) ).
fof(f39_nnf,plain,
! [X,Y,Z,W,U] :
( ~ on(U,Z)
| ~ on(U,Y)
| ~ on(U,X)
| ~ consecutive(Z,W)
| ~ consecutive(Y,Z)
| ~ consecutive(X,Y) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [X,Y,Z,W,U] :
( ~ on(U,Z)
| ~ on(U,Y)
| ~ on(U,X)
| ~ consecutive(Z,W)
| ~ consecutive(Y,Z)
| ~ consecutive(X,Y) ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c39,plain,
( ~ on(X4,X2)
| ~ on(X4,X1)
| ~ on(X4,X0)
| ~ consecutive(X2,X3)
| ~ consecutive(X1,X2)
| ~ consecutive(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(f7,axiom,
consecutive(tuesday,wednesday),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wednesday_follows_tuesday) ).
fof(f7_nnf,plain,
consecutive(tuesday,wednesday),
inference(nnf_transformation,[status(thm)],[f7]) ).
cnf(c7,plain,
consecutive(tuesday,wednesday),
inference(cnf_transformation,[status(esa)],[f7_nnf]) ).
cnf(p60,plain,
( ~ on(X2,X0)
| ~ on(X2,wednesday)
| ~ on(X2,tuesday)
| ~ consecutive(X0,X1)
| ~ consecutive(wednesday,X0) ),
inference(resolution,[status(thm)],[c39,c7]) ).
cnf(f8,axiom,
consecutive(wednesday,thursday),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thursday_follows_wednesday) ).
fof(f8_nnf,plain,
consecutive(wednesday,thursday),
inference(nnf_transformation,[status(thm)],[f8]) ).
cnf(c8,plain,
consecutive(wednesday,thursday),
inference(cnf_transformation,[status(esa)],[f8_nnf]) ).
cnf(p143,plain,
( ~ on(X1,thursday)
| ~ on(X1,wednesday)
| ~ on(X1,tuesday)
| ~ consecutive(thursday,X0) ),
inference(resolution,[status(thm)],[p60,c8]) ).
cnf(f9,axiom,
consecutive(thursday,friday),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',friday_follows_thursday) ).
fof(f9_nnf,plain,
consecutive(thursday,friday),
inference(nnf_transformation,[status(thm)],[f9]) ).
cnf(c9,plain,
consecutive(thursday,friday),
inference(cnf_transformation,[status(esa)],[f9_nnf]) ).
cnf(p153,plain,
( ~ on(X0,thursday)
| ~ on(X0,wednesday)
| ~ on(X0,tuesday) ),
inference(resolution,[status(thm)],[p143,c9]) ).
cnf(p158,plain,
( same_day(X2,tuesday)
| same_person(X1,X0)
| on(X0,X2)
| on(X1,tuesday)
| on(X1,X2)
| ~ on(X0,thursday)
| ~ on(X0,wednesday) ),
inference(resolution,[status(thm)],[p153,c40]) ).
cnf(f38,hypothesis,
( all_on(saturday)
| all_on(friday)
| all_on(thursday)
| all_on(wednesday)
| all_on(tuesday)
| all_on(monday)
| all_on(sunday) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',all_on_one_day) ).
fof(f38_nnf,plain,
( all_on(saturday)
| all_on(friday)
| all_on(thursday)
| all_on(wednesday)
| all_on(tuesday)
| all_on(monday)
| all_on(sunday) ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
( all_on(saturday)
| all_on(friday)
| all_on(thursday)
| all_on(wednesday)
| all_on(tuesday)
| all_on(monday)
| all_on(sunday) ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c38,plain,
( all_on(saturday)
| all_on(friday)
| all_on(thursday)
| all_on(wednesday)
| all_on(tuesday)
| all_on(monday)
| all_on(sunday) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(f1,axiom,
( on(b,X)
| ~ all_on(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',all_on_b_on) ).
fof(f1_nnf,plain,
! [X] :
( on(b,X)
| ~ all_on(X) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X] :
( on(b,X)
| ~ all_on(X) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( on(b,X0)
| ~ all_on(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p49,plain,
( on(b,saturday)
| all_on(friday)
| all_on(thursday)
| all_on(wednesday)
| all_on(tuesday)
| all_on(monday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[c38,c1]) ).
cnf(f45,hypothesis,
~ on(b,saturday),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_off_saturday) ).
fof(f45_nnf,plain,
~ on(b,saturday),
inference(nnf_transformation,[status(thm)],[f45]) ).
fof(f45_sk,plain,
~ on(b,saturday),
inference(skolemisation,[status(esa)],[f45_nnf]) ).
cnf(c45,plain,
~ on(b,saturday),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(p129,plain,
( all_on(friday)
| all_on(thursday)
| all_on(wednesday)
| all_on(tuesday)
| all_on(monday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p49,c45]) ).
cnf(f47,negated_conjecture,
~ all_on(friday),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_all_on_friday) ).
fof(f47_nnf,plain,
~ all_on(friday),
inference(nnf_transformation,[status(thm)],[f47]) ).
fof(f47_sk,plain,
~ all_on(friday),
inference(skolemisation,[status(esa)],[f47_nnf]) ).
cnf(c47,plain,
~ all_on(friday),
inference(cnf_transformation,[status(esa)],[f47_sk]) ).
cnf(p130,plain,
( all_on(thursday)
| all_on(wednesday)
| all_on(tuesday)
| all_on(monday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p129,c47]) ).
cnf(f0,axiom,
( on(a,X)
| ~ all_on(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',all_on_a_on) ).
fof(f0_nnf,plain,
! [X] :
( on(a,X)
| ~ all_on(X) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X] :
( on(a,X)
| ~ all_on(X) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( on(a,X0)
| ~ all_on(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p132,plain,
( on(a,thursday)
| all_on(wednesday)
| all_on(tuesday)
| all_on(monday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p130,c0]) ).
cnf(f43,hypothesis,
~ on(a,thursday),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_off_thursday) ).
fof(f43_nnf,plain,
~ on(a,thursday),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
~ on(a,thursday),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c43,plain,
~ on(a,thursday),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(p136,plain,
( all_on(wednesday)
| all_on(tuesday)
| all_on(monday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p132,c43]) ).
cnf(f2,axiom,
( on(c,X)
| ~ all_on(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',all_on_c_on) ).
fof(f2_nnf,plain,
! [X] :
( on(c,X)
| ~ all_on(X) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X] :
( on(c,X)
| ~ all_on(X) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( on(c,X0)
| ~ all_on(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p139,plain,
( on(c,wednesday)
| all_on(tuesday)
| all_on(monday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p136,c2]) ).
cnf(p2116,plain,
( all_on(tuesday)
| all_on(monday)
| all_on(sunday)
| same_day(X1,tuesday)
| same_person(X0,c)
| on(c,X1)
| on(X0,tuesday)
| on(X0,X1)
| ~ on(c,thursday) ),
inference(resolution,[status(thm)],[p158,p139]) ).
cnf(p5313,plain,
( all_on(tuesday)
| all_on(monday)
| all_on(sunday)
| same_day(X1,tuesday)
| same_person(X0,c)
| on(c,X1)
| on(X0,tuesday)
| on(X0,X1)
| on(c,sunday)
| on(a,thursday)
| on(a,sunday) ),
inference(resolution,[status(thm)],[p249,p2116]) ).
cnf(p5725,plain,
( all_on(tuesday)
| all_on(monday)
| all_on(sunday)
| same_day(sunday,tuesday)
| same_person(a,c)
| on(c,sunday)
| on(a,tuesday)
| on(c,sunday)
| on(a,thursday)
| on(a,sunday) ),
inference(factoring,[status(thm)],[p5313]) ).
cnf(p5731,plain,
( all_on(tuesday)
| all_on(monday)
| all_on(sunday)
| same_day(sunday,tuesday)
| same_person(a,c)
| on(a,tuesday)
| on(c,sunday)
| on(a,thursday)
| on(a,sunday) ),
inference(factoring,[status(thm)],[p5725]) ).
cnf(p5843,plain,
( all_on(tuesday)
| all_on(monday)
| all_on(sunday)
| same_day(sunday,tuesday)
| on(a,tuesday)
| on(c,sunday)
| on(a,thursday)
| on(a,sunday) ),
inference(resolution,[status(thm)],[p5731,c14]) ).
cnf(f18,axiom,
~ same_day(sunday,tuesday),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sunday_not_tuesday) ).
fof(f18_nnf,plain,
~ same_day(sunday,tuesday),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
~ same_day(sunday,tuesday),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
~ same_day(sunday,tuesday),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p5844,plain,
( all_on(tuesday)
| all_on(monday)
| all_on(sunday)
| on(a,tuesday)
| on(c,sunday)
| on(a,thursday)
| on(a,sunday) ),
inference(resolution,[status(thm)],[p5843,c18]) ).
cnf(f46,hypothesis,
~ on(c,sunday),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_off_sunday) ).
fof(f46_nnf,plain,
~ on(c,sunday),
inference(nnf_transformation,[status(thm)],[f46]) ).
fof(f46_sk,plain,
~ on(c,sunday),
inference(skolemisation,[status(esa)],[f46_nnf]) ).
cnf(c46,plain,
~ on(c,sunday),
inference(cnf_transformation,[status(esa)],[f46_sk]) ).
cnf(p5845,plain,
( all_on(tuesday)
| all_on(monday)
| all_on(sunday)
| on(a,tuesday)
| on(a,thursday)
| on(a,sunday) ),
inference(resolution,[status(thm)],[p5844,c46]) ).
cnf(p5846,plain,
( all_on(tuesday)
| all_on(monday)
| all_on(sunday)
| on(a,tuesday)
| on(a,sunday) ),
inference(resolution,[status(thm)],[p5845,c43]) ).
cnf(f42,hypothesis,
~ on(a,tuesday),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_off_tuesday) ).
fof(f42_nnf,plain,
~ on(a,tuesday),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
~ on(a,tuesday),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c42,plain,
~ on(a,tuesday),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(p5959,plain,
( all_on(tuesday)
| all_on(monday)
| all_on(sunday)
| on(a,sunday) ),
inference(resolution,[status(thm)],[p5846,c42]) ).
cnf(f41,hypothesis,
~ on(a,sunday),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_off_sunday) ).
fof(f41_nnf,plain,
~ on(a,sunday),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
~ on(a,sunday),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c41,plain,
~ on(a,sunday),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p5960,plain,
( all_on(tuesday)
| all_on(monday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p5959,c41]) ).
cnf(p5961,plain,
( on(a,tuesday)
| all_on(monday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p5960,c0]) ).
cnf(p5965,plain,
( all_on(monday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p5961,c42]) ).
cnf(p5969,plain,
( on(c,monday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p5965,c2]) ).
cnf(f6,axiom,
consecutive(monday,tuesday),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tuesday_follows_monday) ).
fof(f6_nnf,plain,
consecutive(monday,tuesday),
inference(nnf_transformation,[status(thm)],[f6]) ).
cnf(c6,plain,
consecutive(monday,tuesday),
inference(cnf_transformation,[status(esa)],[f6_nnf]) ).
cnf(p59,plain,
( ~ on(X2,X0)
| ~ on(X2,tuesday)
| ~ on(X2,monday)
| ~ consecutive(X0,X1)
| ~ consecutive(tuesday,X0) ),
inference(resolution,[status(thm)],[c39,c6]) ).
cnf(p141,plain,
( ~ on(X1,wednesday)
| ~ on(X1,tuesday)
| ~ on(X1,monday)
| ~ consecutive(wednesday,X0) ),
inference(resolution,[status(thm)],[p59,c7]) ).
cnf(p148,plain,
( ~ on(X0,wednesday)
| ~ on(X0,tuesday)
| ~ on(X0,monday) ),
inference(resolution,[status(thm)],[p141,c8]) ).
cnf(p5976,plain,
( ~ on(c,wednesday)
| ~ on(c,tuesday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p5969,p148]) ).
cnf(p247,plain,
( on(c,tuesday)
| on(c,sunday)
| on(a,tuesday)
| on(a,sunday) ),
inference(resolution,[status(thm)],[p69,c18]) ).
cnf(p6019,plain,
( on(c,sunday)
| on(a,tuesday)
| on(a,sunday)
| ~ on(c,wednesday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p5976,p247]) ).
cnf(f15,axiom,
~ same_person(b,c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_not_c) ).
fof(f15_nnf,plain,
~ same_person(b,c),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
~ same_person(b,c),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
~ same_person(b,c),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p70,plain,
( same_day(X0,X1)
| on(c,X1)
| on(c,X0)
| on(b,X1)
| on(b,X0) ),
inference(resolution,[status(thm)],[c40,c15]) ).
cnf(f19,axiom,
~ same_day(sunday,wednesday),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sunday_not_wednesday) ).
fof(f19_nnf,plain,
~ same_day(sunday,wednesday),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
~ same_day(sunday,wednesday),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
~ same_day(sunday,wednesday),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(p278,plain,
( on(c,wednesday)
| on(c,sunday)
| on(b,wednesday)
| on(b,sunday) ),
inference(resolution,[status(thm)],[p70,c19]) ).
cnf(p6056,plain,
( on(c,sunday)
| on(b,wednesday)
| on(b,sunday)
| on(c,sunday)
| on(a,tuesday)
| on(a,sunday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p6019,p278]) ).
cnf(p6793,plain,
( on(b,wednesday)
| on(b,sunday)
| on(c,sunday)
| on(a,tuesday)
| on(a,sunday)
| all_on(sunday) ),
inference(factoring,[status(thm)],[p6056]) ).
cnf(p6794,plain,
( on(b,wednesday)
| on(b,sunday)
| on(a,tuesday)
| on(a,sunday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p6793,c46]) ).
cnf(p5968,plain,
( on(b,monday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p5965,c1]) ).
cnf(p5971,plain,
( ~ on(b,wednesday)
| ~ on(b,tuesday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p5968,p148]) ).
cnf(f13,axiom,
~ same_person(a,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_not_b) ).
fof(f13_nnf,plain,
~ same_person(a,b),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
~ same_person(a,b),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
~ same_person(a,b),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p68,plain,
( same_day(X0,X1)
| on(b,X1)
| on(b,X0)
| on(a,X1)
| on(a,X0) ),
inference(resolution,[status(thm)],[c40,c13]) ).
cnf(p226,plain,
( on(b,tuesday)
| on(b,sunday)
| on(a,tuesday)
| on(a,sunday) ),
inference(resolution,[status(thm)],[p68,c18]) ).
cnf(p5998,plain,
( on(b,sunday)
| on(a,tuesday)
| on(a,sunday)
| ~ on(b,wednesday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p5971,p226]) ).
cnf(p6799,plain,
( on(b,sunday)
| on(a,tuesday)
| on(a,sunday)
| all_on(sunday)
| on(b,sunday)
| on(a,tuesday)
| on(a,sunday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p6794,p5998]) ).
cnf(p6852,plain,
( on(b,sunday)
| on(a,tuesday)
| all_on(sunday)
| on(b,sunday)
| on(a,tuesday)
| on(a,sunday)
| all_on(sunday) ),
inference(factoring,[status(thm)],[p6799]) ).
cnf(p6856,plain,
( on(b,sunday)
| all_on(sunday)
| on(b,sunday)
| on(a,tuesday)
| on(a,sunday)
| all_on(sunday) ),
inference(factoring,[status(thm)],[p6852]) ).
cnf(p6859,plain,
( all_on(sunday)
| on(b,sunday)
| on(a,tuesday)
| on(a,sunday)
| all_on(sunday) ),
inference(factoring,[status(thm)],[p6856]) ).
cnf(p6860,plain,
( on(b,sunday)
| on(a,tuesday)
| on(a,sunday)
| all_on(sunday) ),
inference(factoring,[status(thm)],[p6859]) ).
cnf(f5,axiom,
consecutive(sunday,monday),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',monday_follows_sunday) ).
fof(f5_nnf,plain,
consecutive(sunday,monday),
inference(nnf_transformation,[status(thm)],[f5]) ).
cnf(c5,plain,
consecutive(sunday,monday),
inference(cnf_transformation,[status(esa)],[f5_nnf]) ).
cnf(p58,plain,
( ~ on(X2,X0)
| ~ on(X2,monday)
| ~ on(X2,sunday)
| ~ consecutive(X0,X1)
| ~ consecutive(monday,X0) ),
inference(resolution,[status(thm)],[c39,c5]) ).
cnf(p131,plain,
( ~ on(X1,tuesday)
| ~ on(X1,monday)
| ~ on(X1,sunday)
| ~ consecutive(tuesday,X0) ),
inference(resolution,[status(thm)],[p58,c6]) ).
cnf(p142,plain,
( ~ on(X0,tuesday)
| ~ on(X0,monday)
| ~ on(X0,sunday) ),
inference(resolution,[status(thm)],[p131,c7]) ).
cnf(p6868,plain,
( ~ on(b,tuesday)
| ~ on(b,monday)
| on(a,tuesday)
| on(a,sunday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p6860,p142]) ).
cnf(p6873,plain,
( all_on(sunday)
| ~ on(b,tuesday)
| on(a,tuesday)
| on(a,sunday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p6868,p5968]) ).
cnf(p6874,plain,
( ~ on(b,tuesday)
| on(a,tuesday)
| on(a,sunday)
| all_on(sunday) ),
inference(factoring,[status(thm)],[p6873]) ).
cnf(p105,plain,
( same_day(X0,thursday)
| same_person(a,X1)
| on(X1,thursday)
| on(X1,X0)
| on(a,X0) ),
inference(resolution,[status(thm)],[c40,c43]) ).
cnf(p6880,plain,
( same_day(tuesday,thursday)
| same_person(a,b)
| on(b,thursday)
| on(a,tuesday)
| on(a,tuesday)
| on(a,sunday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p6874,p105]) ).
cnf(p6891,plain,
( same_day(tuesday,thursday)
| same_person(a,b)
| on(b,thursday)
| on(a,tuesday)
| on(a,sunday)
| all_on(sunday) ),
inference(factoring,[status(thm)],[p6880]) ).
cnf(p6899,plain,
( same_day(tuesday,thursday)
| on(b,thursday)
| on(a,tuesday)
| on(a,sunday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p6891,c13]) ).
cnf(f29,axiom,
~ same_day(tuesday,thursday),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tuesday_not_thursday) ).
fof(f29_nnf,plain,
~ same_day(tuesday,thursday),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
~ same_day(tuesday,thursday),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
~ same_day(tuesday,thursday),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(p6900,plain,
( on(b,thursday)
| on(a,tuesday)
| on(a,sunday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p6899,c29]) ).
cnf(f44,hypothesis,
~ on(b,thursday),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_off_thursday) ).
fof(f44_nnf,plain,
~ on(b,thursday),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
~ on(b,thursday),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c44,plain,
~ on(b,thursday),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(p6901,plain,
( on(a,tuesday)
| on(a,sunday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p6900,c44]) ).
cnf(p6903,plain,
( on(a,sunday)
| all_on(sunday) ),
inference(resolution,[status(thm)],[p6901,c42]) ).
cnf(p6910,plain,
all_on(sunday),
inference(resolution,[status(thm)],[p6903,c41]) ).
cnf(p6911,plain,
on(a,sunday),
inference(resolution,[status(thm)],[p6910,c0]) ).
cnf(p6915,plain,
$false,
inference(resolution,[status(thm)],[p6911,c41]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ018-1 : TPTP v9.3.1. Bugfixed v1.2.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n017.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Thu Sep 24 06:33:31 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 218.37/74.55 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 218.37/74.55 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------