%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : PUZ005-1 : TPTP v8.1.0. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n018.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:27:11 EDT 2022
% Result : Unsatisfiable 0.20s 0.43s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 21
% Syntax : Number of clauses : 57 ( 23 unt; 18 nHn; 57 RR)
% Number of literals : 109 ( 0 equ; 39 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 10 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-1 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(5,axiom,
( ~ friday(u)
| ~ monday(u) ),
file('PUZ005-1.p',unknown),
[] ).
cnf(6,axiom,
( ~ saturday(u)
| ~ monday(u) ),
file('PUZ005-1.p',unknown),
[] ).
cnf(10,axiom,
( ~ friday(u)
| ~ tuesday(u) ),
file('PUZ005-1.p',unknown),
[] ).
cnf(11,axiom,
( ~ saturday(u)
| ~ tuesday(u) ),
file('PUZ005-1.p',unknown),
[] ).
cnf(14,axiom,
( ~ friday(u)
| ~ wednesday(u) ),
file('PUZ005-1.p',unknown),
[] ).
cnf(15,axiom,
( ~ saturday(u)
| ~ wednesday(u) ),
file('PUZ005-1.p',unknown),
[] ).
cnf(21,axiom,
( ~ sunday(u)
| ~ friday(u) ),
file('PUZ005-1.p',unknown),
[] ).
cnf(22,axiom,
( ~ sunday(u)
| ~ saturday(u) ),
file('PUZ005-1.p',unknown),
[] ).
cnf(23,axiom,
( ~ monday(yesterday(u))
| tuesday(u) ),
file('PUZ005-1.p',unknown),
[] ).
cnf(24,axiom,
( ~ tuesday(yesterday(u))
| wednesday(u) ),
file('PUZ005-1.p',unknown),
[] ).
cnf(25,axiom,
( ~ wednesday(yesterday(u))
| thursday(u) ),
file('PUZ005-1.p',unknown),
[] ).
cnf(26,axiom,
( ~ thursday(yesterday(u))
| friday(u) ),
file('PUZ005-1.p',unknown),
[] ).
cnf(30,axiom,
( ~ tuesday(u)
| monday(yesterday(u)) ),
file('PUZ005-1.p',unknown),
[] ).
cnf(31,axiom,
( ~ wednesday(u)
| tuesday(yesterday(u)) ),
file('PUZ005-1.p',unknown),
[] ).
cnf(36,axiom,
( ~ monday(u)
| sunday(yesterday(u)) ),
file('PUZ005-1.p',unknown),
[] ).
cnf(37,axiom,
( ~ member(u,lying_days(lion))
| wednesday(u)
| tuesday(u)
| monday(u) ),
file('PUZ005-1.p',unknown),
[] ).
cnf(38,axiom,
( ~ member(u,lying_days(unicorn))
| saturday(u)
| friday(u)
| thursday(u) ),
file('PUZ005-1.p',unknown),
[] ).
cnf(45,axiom,
( ~ admits(u,v,w)
| member(w,lying_days(u))
| member(v,lying_days(u)) ),
file('PUZ005-1.p',unknown),
[] ).
cnf(49,axiom,
admits(lion,today,yesterday(today)),
file('PUZ005-1.p',unknown),
[] ).
cnf(50,axiom,
admits(unicorn,today,yesterday(today)),
file('PUZ005-1.p',unknown),
[] ).
cnf(51,axiom,
~ thursday(today),
file('PUZ005-1.p',unknown),
[] ).
cnf(53,plain,
( ~ member(today,lying_days(unicorn))
| saturday(today)
| friday(today) ),
inference(res,[status(thm),theory(equality)],[38,51]),
[iquote('0:Res:38.1,51.0')] ).
cnf(54,plain,
~ wednesday(yesterday(today)),
inference(res,[status(thm),theory(equality)],[25,51]),
[iquote('0:Res:25.1,51.0')] ).
cnf(119,plain,
saturday(today),
inference(spt,[spt(split,[position(s1)])],[53]),
[iquote('1:Spt:53.1')] ).
cnf(126,plain,
( member(yesterday(today),lying_days(unicorn))
| member(today,lying_days(unicorn)) ),
inference(res,[status(thm),theory(equality)],[50,45]),
[iquote('0:Res:50.0,45.0')] ).
cnf(127,plain,
( member(yesterday(today),lying_days(lion))
| member(today,lying_days(lion)) ),
inference(res,[status(thm),theory(equality)],[49,45]),
[iquote('0:Res:49.0,45.0')] ).
cnf(130,plain,
( member(today,lying_days(unicorn))
| saturday(yesterday(today))
| friday(yesterday(today))
| thursday(yesterday(today)) ),
inference(res,[status(thm),theory(equality)],[126,38]),
[iquote('0:Res:126.0,38.0')] ).
cnf(131,plain,
( member(today,lying_days(lion))
| wednesday(yesterday(today))
| tuesday(yesterday(today))
| monday(yesterday(today)) ),
inference(res,[status(thm),theory(equality)],[127,37]),
[iquote('0:Res:127.0,37.0')] ).
cnf(132,plain,
( member(today,lying_days(lion))
| tuesday(yesterday(today))
| monday(yesterday(today)) ),
inference(mrr,[status(thm)],[131,54]),
[iquote('0:MRR:131.1,54.0')] ).
cnf(141,plain,
( tuesday(yesterday(today))
| monday(yesterday(today))
| wednesday(today)
| tuesday(today)
| monday(today) ),
inference(res,[status(thm),theory(equality)],[132,37]),
[iquote('0:Res:132.0,37.0')] ).
cnf(142,plain,
( wednesday(today)
| tuesday(today)
| monday(today) ),
inference(mrr,[status(thm)],[141,24,23]),
[iquote('0:MRR:141.0,141.1,24.0,23.0')] ).
cnf(143,plain,
( monday(today)
| tuesday(today) ),
inference(ems,[status(thm)],[15,119,142]),
[iquote('1:EmS:15.0,15.1,119.0,142.0')] ).
cnf(146,plain,
monday(today),
inference(ems,[status(thm)],[11,119,143]),
[iquote('1:EmS:11.0,11.1,119.0,143.1')] ).
cnf(149,plain,
$false,
inference(ems,[status(thm)],[6,119,146]),
[iquote('1:EmS:6.0,6.1,119.0,146.0')] ).
cnf(151,plain,
~ saturday(today),
inference(spt,[spt(split,[position(sa)])],[149,119]),
[iquote('1:Spt:149.0,53.1,119.0')] ).
cnf(152,plain,
( ~ member(today,lying_days(unicorn))
| friday(today) ),
inference(spt,[spt(split,[position(s2)])],[53]),
[iquote('1:Spt:149.0,53.0,53.2')] ).
cnf(160,plain,
( saturday(yesterday(today))
| friday(yesterday(today))
| thursday(yesterday(today))
| friday(today) ),
inference(res,[status(thm),theory(equality)],[130,152]),
[iquote('1:Res:130.0,152.0')] ).
cnf(161,plain,
( saturday(yesterday(today))
| friday(yesterday(today))
| friday(today) ),
inference(mrr,[status(thm)],[160,26]),
[iquote('1:MRR:160.2,26.0')] ).
cnf(162,plain,
saturday(yesterday(today)),
inference(spt,[spt(split,[position(s2s1)])],[161]),
[iquote('2:Spt:161.0')] ).
cnf(165,plain,
~ monday(today),
inference(ems,[status(thm)],[22,36,162]),
[iquote('2:EmS:22.0,22.1,36.1,162.0')] ).
cnf(167,plain,
~ tuesday(today),
inference(ems,[status(thm)],[6,162,30]),
[iquote('2:EmS:6.0,6.1,162.0,30.1')] ).
cnf(168,plain,
~ wednesday(today),
inference(ems,[status(thm)],[11,162,31]),
[iquote('2:EmS:11.0,11.1,162.0,31.1')] ).
cnf(171,plain,
( wednesday(today)
| tuesday(today) ),
inference(mrr,[status(thm)],[142,165]),
[iquote('2:MRR:142.2,165.0')] ).
cnf(173,plain,
$false,
inference(mrr,[status(thm)],[171,168,167]),
[iquote('2:MRR:171.0,171.1,168.0,167.0')] ).
cnf(175,plain,
~ saturday(yesterday(today)),
inference(spt,[spt(split,[position(s2sa)])],[173,162]),
[iquote('2:Spt:173.0,161.0,162.0')] ).
cnf(176,plain,
( friday(yesterday(today))
| friday(today) ),
inference(spt,[spt(split,[position(s2s2)])],[161]),
[iquote('2:Spt:173.0,161.1,161.2')] ).
cnf(178,plain,
friday(yesterday(today)),
inference(spt,[spt(split,[position(s2s2s1)])],[176]),
[iquote('3:Spt:176.0')] ).
cnf(181,plain,
~ monday(today),
inference(ems,[status(thm)],[21,36,178]),
[iquote('3:EmS:21.0,21.1,36.1,178.0')] ).
cnf(183,plain,
~ tuesday(today),
inference(ems,[status(thm)],[5,178,30]),
[iquote('3:EmS:5.0,5.1,178.0,30.1')] ).
cnf(184,plain,
~ wednesday(today),
inference(ems,[status(thm)],[10,178,31]),
[iquote('3:EmS:10.0,10.1,178.0,31.1')] ).
cnf(188,plain,
( wednesday(today)
| tuesday(today) ),
inference(mrr,[status(thm)],[142,181]),
[iquote('3:MRR:142.2,181.0')] ).
cnf(190,plain,
$false,
inference(mrr,[status(thm)],[188,184,183]),
[iquote('3:MRR:188.0,188.1,184.0,183.0')] ).
cnf(192,plain,
~ friday(yesterday(today)),
inference(spt,[spt(split,[position(s2s2sa)])],[190,178]),
[iquote('3:Spt:190.0,176.0,178.0')] ).
cnf(193,plain,
friday(today),
inference(spt,[spt(split,[position(s2s2s2)])],[176]),
[iquote('3:Spt:190.0,176.1')] ).
cnf(199,plain,
( monday(today)
| tuesday(today) ),
inference(ems,[status(thm)],[14,193,142]),
[iquote('3:EmS:14.0,14.1,193.0,142.0')] ).
cnf(202,plain,
monday(today),
inference(ems,[status(thm)],[10,193,199]),
[iquote('3:EmS:10.0,10.1,193.0,199.1')] ).
cnf(209,plain,
$false,
inference(ems,[status(thm)],[5,193,202]),
[iquote('3:EmS:5.0,5.1,193.0,202.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : PUZ005-1 : TPTP v8.1.0. Released v1.0.0.
% 0.12/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n018.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 : 600
% 0.13/0.34 % DateTime : Sat May 28 21:21:40 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.20/0.43
% 0.20/0.43 SPASS V 3.9
% 0.20/0.43 SPASS beiseite: Proof found.
% 0.20/0.43 % SZS status Theorem
% 0.20/0.43 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.43 SPASS derived 104 clauses, backtracked 17 clauses, performed 3 splits and kept 104 clauses.
% 0.20/0.43 SPASS allocated 75697 KBytes.
% 0.20/0.43 SPASS spent 0:00:00.07 on the problem.
% 0.20/0.43 0:00:00.04 for the input.
% 0.20/0.43 0:00:00.00 for the FLOTTER CNF translation.
% 0.20/0.43 0:00:00.00 for inferences.
% 0.20/0.43 0:00:00.00 for the backtracking.
% 0.20/0.43 0:00:00.00 for the reduction.
% 0.20/0.43
% 0.20/0.43
% 0.20/0.43 Here is a proof with depth 8, length 57 :
% 0.20/0.43 % SZS output start Refutation
% See solution above
% 0.20/0.43 Formulae used in the proof : monday_not_friday monday_not_saturday tuesday_not_friday tuesday_not_saturday wednesday_not_friday wednesday_not_saturday friday_not_sunday saturday_not_sunday monday_yesterday tuesday_yesterday wednesday_yesterday thursday_yesterday yesterday_monday yesterday_tuesday yesterday_sunday lions_lying_days unicorns_lying_days admissions1 admissions5 admissions6 prove_today_is_thursday
% 0.20/0.43
%------------------------------------------------------------------------------