%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PUZ018-1 : TPTP v8.1.2. Bugfixed v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.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:36 EDT 2024
% Result : Unsatisfiable 33.80s 34.01s
% Output : Refutation 33.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 23
% Syntax : Number of clauses : 62 ( 25 unt; 24 nHn; 53 RR)
% Number of literals : 163 ( 0 equ; 51 neg)
% Maximal clause size : 7 ( 2 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 : 34 ( 7 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(wednesday_follows_tuesday,axiom,
consecutive(tuesday,wednesday),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wednesday_follows_tuesday) ).
cnf(thursday_follows_wednesday,axiom,
consecutive(wednesday,thursday),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thursday_follows_wednesday) ).
cnf(friday_follows_thursday,axiom,
consecutive(thursday,friday),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',friday_follows_thursday) ).
cnf(a_not_c,axiom,
~ same_person(a,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_not_c) ).
cnf(c_off_sunday,plain,
~ on(c,sunday),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c_off_sunday) ).
cnf(sunday_not_tuesday,axiom,
~ same_day(sunday,tuesday),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sunday_not_tuesday) ).
cnf(a_off_tuesday,plain,
~ on(a,tuesday),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_off_tuesday) ).
cnf(a_off_sunday,plain,
~ on(a,sunday),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_off_sunday) ).
cnf(no_two_off_twice_together,plain,
( on(X28,X29)
| on(X28,X30)
| on(X27,X29)
| on(X27,X30)
| same_person(X28,X27)
| same_day(X29,X30) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',no_two_off_twice_together) ).
cnf(c48,plain,
( on(a,X141)
| on(X140,sunday)
| on(X140,X141)
| same_person(a,X140)
| same_day(sunday,X141) ),
inference(resolution,[status(thm)],[no_two_off_twice_together,a_off_sunday]) ).
cnf(c1904,plain,
( on(X424,sunday)
| on(X424,tuesday)
| same_person(a,X424)
| same_day(sunday,tuesday) ),
inference(resolution,[status(thm)],[c48,a_off_tuesday]) ).
cnf(c7549,plain,
( on(X425,sunday)
| on(X425,tuesday)
| same_person(a,X425) ),
inference(resolution,[status(thm)],[c1904,sunday_not_tuesday]) ).
cnf(c7561,plain,
( on(c,tuesday)
| same_person(a,c) ),
inference(resolution,[status(thm)],[c7549,c_off_sunday]) ).
cnf(c7608,plain,
on(c,tuesday),
inference(resolution,[status(thm)],[c7561,a_not_c]) ).
cnf(not_on_for_3_days,plain,
( ~ consecutive(X13,X14)
| ~ consecutive(X14,X11)
| ~ consecutive(X11,X15)
| ~ on(X12,X13)
| ~ on(X12,X14)
| ~ on(X12,X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_on_for_3_days) ).
cnf(sunday_not_thursday,axiom,
~ same_day(sunday,thursday),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sunday_not_thursday) ).
cnf(a_off_thursday,plain,
~ on(a,thursday),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_off_thursday) ).
cnf(c1902,plain,
( on(X378,sunday)
| on(X378,thursday)
| same_person(a,X378)
| same_day(sunday,thursday) ),
inference(resolution,[status(thm)],[c48,a_off_thursday]) ).
cnf(c6211,plain,
( on(X379,sunday)
| on(X379,thursday)
| same_person(a,X379) ),
inference(resolution,[status(thm)],[c1902,sunday_not_thursday]) ).
cnf(c6221,plain,
( on(c,thursday)
| same_person(a,c) ),
inference(resolution,[status(thm)],[c6211,c_off_sunday]) ).
cnf(c6347,plain,
on(c,thursday),
inference(resolution,[status(thm)],[c6221,a_not_c]) ).
cnf(c6357,plain,
( ~ consecutive(X1293,X1294)
| ~ consecutive(X1294,thursday)
| ~ consecutive(thursday,X1292)
| ~ on(c,X1293)
| ~ on(c,X1294) ),
inference(resolution,[status(thm)],[c6347,not_on_for_3_days]) ).
cnf(all_on_c_on,axiom,
( ~ all_on(X6)
| on(c,X6) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',all_on_c_on) ).
cnf(monday_follows_sunday,axiom,
consecutive(sunday,monday),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',monday_follows_sunday) ).
cnf(tuesday_follows_monday,axiom,
consecutive(monday,tuesday),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tuesday_follows_monday) ).
cnf(a_not_b,axiom,
~ same_person(a,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_not_b) ).
cnf(b_off_thursday,plain,
~ on(b,thursday),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b_off_thursday) ).
cnf(c6249,plain,
( on(b,sunday)
| same_person(a,b) ),
inference(resolution,[status(thm)],[c6211,b_off_thursday]) ).
cnf(c6461,plain,
on(b,sunday),
inference(resolution,[status(thm)],[c6249,a_not_b]) ).
cnf(all_on_b_on,axiom,
( ~ all_on(X5)
| on(b,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',all_on_b_on) ).
cnf(b_off_saturday,plain,
~ on(b,saturday),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b_off_saturday) ).
cnf(all_on_a_on,axiom,
( ~ all_on(X4)
| on(a,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',all_on_a_on) ).
cnf(prove_all_on_friday,negated_conjecture,
~ all_on(friday),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_all_on_friday) ).
cnf(all_on_one_day,plain,
( all_on(sunday)
| all_on(monday)
| all_on(tuesday)
| all_on(wednesday)
| all_on(thursday)
| all_on(friday)
| all_on(saturday) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',all_on_one_day) ).
cnf(c1,plain,
( all_on(monday)
| all_on(tuesday)
| all_on(wednesday)
| all_on(thursday)
| all_on(friday)
| all_on(saturday)
| on(c,sunday) ),
inference(resolution,[status(thm)],[all_on_one_day,all_on_c_on]) ).
cnf(c123,plain,
( all_on(monday)
| all_on(tuesday)
| all_on(wednesday)
| all_on(thursday)
| all_on(saturday)
| on(c,sunday) ),
inference(resolution,[status(thm)],[c1,prove_all_on_friday]) ).
cnf(c9708,plain,
( all_on(monday)
| all_on(tuesday)
| all_on(wednesday)
| all_on(thursday)
| all_on(saturday) ),
inference(resolution,[status(thm)],[c123,c_off_sunday]) ).
cnf(c9731,plain,
( all_on(monday)
| all_on(wednesday)
| all_on(thursday)
| all_on(saturday)
| on(a,tuesday) ),
inference(resolution,[status(thm)],[c9708,all_on_a_on]) ).
cnf(c18922,plain,
( all_on(monday)
| all_on(wednesday)
| all_on(thursday)
| all_on(saturday) ),
inference(resolution,[status(thm)],[c9731,a_off_tuesday]) ).
cnf(c18968,plain,
( all_on(monday)
| all_on(wednesday)
| all_on(saturday)
| on(a,thursday) ),
inference(resolution,[status(thm)],[c18922,all_on_a_on]) ).
cnf(c19409,plain,
( all_on(monday)
| all_on(wednesday)
| all_on(saturday) ),
inference(resolution,[status(thm)],[c18968,a_off_thursday]) ).
cnf(c19448,plain,
( all_on(monday)
| all_on(wednesday)
| on(b,saturday) ),
inference(resolution,[status(thm)],[c19409,all_on_b_on]) ).
cnf(c20100,plain,
( all_on(monday)
| all_on(wednesday) ),
inference(resolution,[status(thm)],[c19448,b_off_saturday]) ).
cnf(c20125,plain,
( all_on(wednesday)
| on(b,monday) ),
inference(resolution,[status(thm)],[c20100,all_on_b_on]) ).
cnf(tuesday_not_thursday,axiom,
~ same_day(tuesday,thursday),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tuesday_not_thursday) ).
cnf(c45,plain,
( on(a,X127)
| on(X126,tuesday)
| on(X126,X127)
| same_person(a,X126)
| same_day(tuesday,X127) ),
inference(resolution,[status(thm)],[no_two_off_twice_together,a_off_tuesday]) ).
cnf(c1774,plain,
( on(X272,tuesday)
| on(X272,thursday)
| same_person(a,X272)
| same_day(tuesday,thursday) ),
inference(resolution,[status(thm)],[c45,a_off_thursday]) ).
cnf(c3983,plain,
( on(X278,tuesday)
| on(X278,thursday)
| same_person(a,X278) ),
inference(resolution,[status(thm)],[c1774,tuesday_not_thursday]) ).
cnf(c4024,plain,
( on(b,tuesday)
| same_person(a,b) ),
inference(resolution,[status(thm)],[c3983,b_off_thursday]) ).
cnf(c4043,plain,
on(b,tuesday),
inference(resolution,[status(thm)],[c4024,a_not_b]) ).
cnf(c4056,plain,
( ~ consecutive(X1258,X1259)
| ~ consecutive(X1259,tuesday)
| ~ consecutive(tuesday,X1257)
| ~ on(b,X1258)
| ~ on(b,X1259) ),
inference(resolution,[status(thm)],[c4043,not_on_for_3_days]) ).
cnf(c28639,plain,
( ~ consecutive(X1882,monday)
| ~ consecutive(monday,tuesday)
| ~ consecutive(tuesday,X1883)
| ~ on(b,X1882)
| all_on(wednesday) ),
inference(resolution,[status(thm)],[c4056,c20125]) ).
cnf(c43210,plain,
( ~ consecutive(sunday,monday)
| ~ consecutive(monday,tuesday)
| ~ consecutive(tuesday,X1884)
| all_on(wednesday) ),
inference(resolution,[status(thm)],[c28639,c6461]) ).
cnf(c43340,plain,
( ~ consecutive(sunday,monday)
| ~ consecutive(monday,tuesday)
| all_on(wednesday) ),
inference(resolution,[status(thm)],[c43210,wednesday_follows_tuesday]) ).
cnf(c43341,plain,
( ~ consecutive(sunday,monday)
| all_on(wednesday) ),
inference(resolution,[status(thm)],[c43340,tuesday_follows_monday]) ).
cnf(c43342,plain,
all_on(wednesday),
inference(resolution,[status(thm)],[c43341,monday_follows_sunday]) ).
cnf(c43352,plain,
on(c,wednesday),
inference(resolution,[status(thm)],[c43342,all_on_c_on]) ).
cnf(c43443,plain,
( ~ consecutive(X1943,wednesday)
| ~ consecutive(wednesday,thursday)
| ~ consecutive(thursday,X1944)
| ~ on(c,X1943) ),
inference(resolution,[status(thm)],[c43352,c6357]) ).
cnf(c44712,plain,
( ~ consecutive(tuesday,wednesday)
| ~ consecutive(wednesday,thursday)
| ~ consecutive(thursday,X1945) ),
inference(resolution,[status(thm)],[c43443,c7608]) ).
cnf(c44921,plain,
( ~ consecutive(tuesday,wednesday)
| ~ consecutive(wednesday,thursday) ),
inference(resolution,[status(thm)],[c44712,friday_follows_thursday]) ).
cnf(c44922,plain,
~ consecutive(tuesday,wednesday),
inference(resolution,[status(thm)],[c44921,thursday_follows_wednesday]) ).
cnf(c44923,plain,
$false,
inference(resolution,[status(thm)],[c44922,wednesday_follows_tuesday]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : PUZ018-1 : TPTP v8.1.2. Bugfixed v1.2.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n023.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % 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:41:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 33.80/34.01 % Version: 1.5
% 33.80/34.01 % SZS status Unsatisfiable
% 33.80/34.01 % SZS output start CNFRefutation
% See solution above
% 33.80/34.01
% 33.80/34.01 % Initial clauses : 48
% 33.80/34.01 % Processed clauses : 805
% 33.80/34.01 % Factors computed : 359
% 33.80/34.01 % Resolvents computed: 44565
% 33.80/34.01 % Tautologies deleted: 9
% 33.80/34.01 % Forward subsumed : 2530
% 33.80/34.01 % Backward subsumed : 520
% 33.80/34.01 % -------- CPU Time ---------
% 33.80/34.01 % User time : 33.519 s
% 33.80/34.01 % System time : 0.149 s
% 33.80/34.01 % Total time : 33.668 s
%------------------------------------------------------------------------------