%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : PUZ005-1 : TPTP v9.0.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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 : Fri Jul 25 01:24:24 PM UTC 2025
% Result : Unsatisfiable 48.64s 6.44s
% Output : CNFRefutation 48.64s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named prove_today_is_thursday)
% Comments :
%------------------------------------------------------------------------------
cnf(50,plain,
~ thursday(today),
inference(cnf,[status(esa)],[prove_today_is_thursday]) ).
cnf(l0,plain,
~ thursday(today),
inference(instantiation,[status(thm)],[50]) ).
cnf(0,plain,
( thursday(X0)
| monday(X0)
| tuesday(X0)
| wednesday(X0)
| friday(X0)
| saturday(X0)
| sunday(X0) ),
inference(cnf,[status(esa)],[it_is_a_day]) ).
cnf(l1,plain,
( thursday(today)
| monday(today)
| tuesday(today)
| wednesday(today)
| friday(today)
| saturday(today)
| sunday(today) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(5,plain,
( ~ monday(X0)
| ~ saturday(X0) ),
inference(cnf,[status(esa)],[monday_not_saturday]) ).
cnf(l91,plain,
( ~ monday(today)
| ~ saturday(today) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(32,plain,
( ~ friday(X0)
| thursday(yesterday(X0)) ),
inference(cnf,[status(esa)],[yesterday_thursday]) ).
cnf(l99,plain,
( ~ friday(today)
| thursday(yesterday(today)) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(9,plain,
( ~ tuesday(X0)
| ~ friday(X0) ),
inference(cnf,[status(esa)],[tuesday_not_friday]) ).
cnf(l98,plain,
( ~ tuesday(today)
| ~ friday(today) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(12,plain,
( ~ thursday(X0)
| ~ wednesday(X0) ),
inference(cnf,[status(esa)],[wednesday_not_thursday]) ).
cnf(l118,plain,
( ~ thursday(yesterday(today))
| ~ wednesday(yesterday(today)) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(43,plain,
( ~ saturday(X0)
| member(X0,lying_days(unicorn)) ),
inference(cnf,[status(esa)],[unicorn_lies_on_saturday]) ).
cnf(l90,plain,
( ~ saturday(today)
| member(today,lying_days(unicorn)) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(15,plain,
( ~ wednesday(X0)
| ~ sunday(X0) ),
inference(cnf,[status(esa)],[wednesday_not_sunday]) ).
cnf(l92,plain,
( ~ wednesday(today)
| ~ sunday(today) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(36,plain,
( ~ member(X0,lying_days(lion))
| monday(X0)
| tuesday(X0)
| wednesday(X0) ),
inference(cnf,[status(esa)],[lions_lying_days]) ).
cnf(l96,plain,
( ~ member(today,lying_days(lion))
| monday(today)
| tuesday(today)
| wednesday(today) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l124,plain,
( ~ member(yesterday(today),lying_days(lion))
| monday(yesterday(today))
| tuesday(yesterday(today))
| wednesday(yesterday(today)) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(37,plain,
( ~ member(X0,lying_days(unicorn))
| thursday(X0)
| friday(X0)
| saturday(X0) ),
inference(cnf,[status(esa)],[unicorns_lying_days]) ).
cnf(l93,plain,
( ~ member(today,lying_days(unicorn))
| thursday(today)
| friday(today)
| saturday(today) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(29,plain,
( ~ tuesday(X0)
| monday(yesterday(X0)) ),
inference(cnf,[status(esa)],[yesterday_monday]) ).
cnf(l207,plain,
( ~ tuesday(today)
| monday(yesterday(today)) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(44,plain,
( ~ admits(X0,X1,X2)
| member(X1,lying_days(X0))
| member(X2,lying_days(X0)) ),
inference(cnf,[status(esa)],[admissions1]) ).
cnf(l125,plain,
( ~ admits(lion,today,yesterday(today))
| member(today,lying_days(lion))
| member(yesterday(today),lying_days(lion)) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(48,plain,
admits(lion,today,yesterday(today)),
inference(cnf,[status(esa)],[admissions5]) ).
cnf(l177,plain,
admits(lion,today,yesterday(today)),
inference(instantiation,[status(thm)],[48]) ).
cnf(6,plain,
( ~ monday(X0)
| ~ sunday(X0) ),
inference(cnf,[status(esa)],[monday_not_sunday]) ).
cnf(l2338,plain,
( ~ monday(today)
| ~ sunday(today) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(14,plain,
( ~ wednesday(X0)
| ~ saturday(X0) ),
inference(cnf,[status(esa)],[wednesday_not_saturday]) ).
cnf(l102,plain,
( ~ wednesday(today)
| ~ saturday(today) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(46,plain,
( ~ member(X0,lying_days(X1))
| ~ member(X2,lying_days(X1))
| ~ admits(X1,X0,X2) ),
inference(cnf,[status(esa)],[admissions3]) ).
cnf(l1211,plain,
( ~ member(yesterday(today),lying_days(unicorn))
| ~ member(today,lying_days(unicorn))
| ~ admits(unicorn,yesterday(today),today) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(3,plain,
( ~ thursday(X0)
| ~ monday(X0) ),
inference(cnf,[status(esa)],[monday_not_thursday]) ).
cnf(l309,plain,
( ~ thursday(yesterday(today))
| ~ monday(yesterday(today)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(26,plain,
( ~ friday(yesterday(X0))
| saturday(X0) ),
inference(cnf,[status(esa)],[friday_yesterday]) ).
cnf(l126,plain,
( ~ friday(yesterday(today))
| saturday(today) ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l210,plain,
( ~ member(yesterday(today),lying_days(unicorn))
| thursday(yesterday(today))
| friday(yesterday(today))
| saturday(yesterday(today)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l230,plain,
( ~ member(today,lying_days(lion))
| monday(today)
| tuesday(today)
| wednesday(today) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(25,plain,
( ~ thursday(yesterday(X0))
| friday(X0) ),
inference(cnf,[status(esa)],[thursday_yesterday]) ).
cnf(l346,plain,
( ~ thursday(yesterday(today))
| friday(today) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l100,plain,
( ~ admits(unicorn,today,yesterday(today))
| member(today,lying_days(unicorn))
| member(yesterday(today),lying_days(unicorn)) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l366,plain,
( ~ tuesday(today)
| ~ friday(today) ),
inference(instantiation,[status(thm)],[9]) ).
cnf(27,plain,
( ~ saturday(yesterday(X0))
| sunday(X0) ),
inference(cnf,[status(esa)],[saturday_yesterday]) ).
cnf(l345,plain,
( ~ saturday(yesterday(today))
| sunday(today) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(49,plain,
admits(unicorn,today,yesterday(today)),
inference(cnf,[status(esa)],[admissions6]) ).
cnf(l106,plain,
admits(unicorn,today,yesterday(today)),
inference(instantiation,[status(thm)],[49]) ).
cnf(l128,plain,
( ~ admits(lion,yesterday(today),today)
| member(yesterday(today),lying_days(lion))
| member(today,lying_days(lion)) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(45,plain,
( ~ member(X0,lying_days(X1))
| member(X2,lying_days(X1))
| admits(X1,X2,X0) ),
inference(cnf,[status(esa)],[admissions2]) ).
cnf(l1450,plain,
( ~ member(today,lying_days(unicorn))
| member(yesterday(today),lying_days(unicorn))
| admits(unicorn,yesterday(today),today) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l216,plain,
( ~ admits(unicorn,today,yesterday(today))
| member(today,lying_days(unicorn))
| member(yesterday(today),lying_days(unicorn)) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(13,plain,
( ~ wednesday(X0)
| ~ friday(X0) ),
inference(cnf,[status(esa)],[wednesday_not_friday]) ).
cnf(l2182,plain,
( ~ wednesday(today)
| ~ friday(today) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l108,plain,
( ~ thursday(yesterday(today))
| friday(today) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(47,plain,
( ~ member(X0,lying_days(X1))
| member(X2,lying_days(X1))
| admits(X1,X0,X2) ),
inference(cnf,[status(esa)],[admissions4]) ).
cnf(l149,plain,
( ~ member(yesterday(today),lying_days(lion))
| member(today,lying_days(lion))
| admits(lion,yesterday(today),today) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l127,plain,
( thursday(yesterday(today))
| monday(yesterday(today))
| tuesday(yesterday(today))
| wednesday(yesterday(today))
| friday(yesterday(today))
| saturday(yesterday(today))
| sunday(yesterday(today)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2682,plain,
( ~ wednesday(today)
| ~ friday(today) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1313,plain,
( ~ saturday(yesterday(today))
| member(yesterday(today),lying_days(unicorn)) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(4,plain,
( ~ monday(X0)
| ~ friday(X0) ),
inference(cnf,[status(esa)],[monday_not_friday]) ).
cnf(l2056,plain,
( ~ monday(today)
| ~ friday(today) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l247,plain,
( ~ monday(today)
| ~ friday(today) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(23,plain,
( ~ tuesday(yesterday(X0))
| wednesday(X0) ),
inference(cnf,[status(esa)],[tuesday_yesterday]) ).
cnf(l308,plain,
( ~ tuesday(yesterday(today))
| wednesday(today) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(39,plain,
( ~ tuesday(X0)
| member(X0,lying_days(lion)) ),
inference(cnf,[status(esa)],[lion_lies_on_tuesday]) ).
cnf(l173,plain,
( ~ tuesday(yesterday(today))
| member(yesterday(today),lying_days(lion)) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l2045,plain,
( ~ wednesday(today)
| ~ sunday(today) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(38,plain,
( ~ monday(X0)
| member(X0,lying_days(lion)) ),
inference(cnf,[status(esa)],[lion_lies_on_monday]) ).
cnf(l265,plain,
( ~ monday(yesterday(today))
| member(yesterday(today),lying_days(lion)) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l157,plain,
( ~ admits(lion,today,yesterday(today))
| member(today,lying_days(lion))
| member(yesterday(today),lying_days(lion)) ),
inference(instantiation,[status(thm)],[44]) ).
cnf(l295,plain,
( ~ member(today,lying_days(lion))
| ~ member(yesterday(today),lying_days(lion))
| ~ admits(lion,today,yesterday(today)) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l220,plain,
admits(unicorn,today,yesterday(today)),
inference(instantiation,[status(thm)],[49]) ).
cnf(l158,plain,
admits(lion,today,yesterday(today)),
inference(instantiation,[status(thm)],[48]) ).
cnf(l262,plain,
( ~ member(today,lying_days(lion))
| ~ member(yesterday(today),lying_days(lion))
| ~ admits(lion,today,yesterday(today)) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l2180,plain,
admits(lion,today,yesterday(today)),
inference(instantiation,[status(thm)],[48]) ).
cnf(l1414,plain,
( ~ monday(yesterday(today))
| ~ saturday(yesterday(today)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(34,plain,
( ~ sunday(X0)
| saturday(yesterday(X0)) ),
inference(cnf,[status(esa)],[yesterday_saturday]) ).
cnf(l1502,plain,
( ~ sunday(today)
| saturday(yesterday(today)) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l256,plain,
( ~ monday(yesterday(today))
| ~ sunday(yesterday(today)) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1574,plain,
( ~ member(yesterday(today),lying_days(unicorn))
| thursday(yesterday(today))
| friday(yesterday(today))
| saturday(yesterday(today)) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l1316,plain,
( thursday(yesterday(today))
| monday(yesterday(today))
| tuesday(yesterday(today))
| wednesday(yesterday(today))
| friday(yesterday(today))
| saturday(yesterday(today))
| sunday(yesterday(today)) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(21,plain,
( ~ saturday(X0)
| ~ sunday(X0) ),
inference(cnf,[status(esa)],[saturday_not_sunday]) ).
cnf(l2746,plain,
( ~ saturday(yesterday(today))
| ~ sunday(yesterday(today)) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l2120,plain,
admits(lion,today,yesterday(today)),
inference(instantiation,[status(thm)],[48]) ).
cnf(l289,plain,
( ~ tuesday(today)
| member(today,lying_days(lion)) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l1460,plain,
( ~ member(today,lying_days(unicorn))
| ~ member(yesterday(today),lying_days(unicorn))
| ~ admits(unicorn,today,yesterday(today)) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l2035,plain,
( ~ tuesday(today)
| member(today,lying_days(lion)) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l150,plain,
( ~ member(yesterday(today),lying_days(lion))
| monday(yesterday(today))
| tuesday(yesterday(today))
| wednesday(yesterday(today)) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l359,plain,
( ~ wednesday(today)
| ~ friday(today) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(40,plain,
( ~ wednesday(X0)
| member(X0,lying_days(lion)) ),
inference(cnf,[status(esa)],[lion_lies_on_wednesday]) ).
cnf(l236,plain,
( ~ wednesday(yesterday(today))
| member(yesterday(today),lying_days(lion)) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(l1329,plain,
( ~ wednesday(yesterday(today))
| ~ friday(yesterday(today)) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(35,plain,
( ~ monday(X0)
| sunday(yesterday(X0)) ),
inference(cnf,[status(esa)],[yesterday_sunday]) ).
cnf(l2763,plain,
( ~ monday(today)
| sunday(yesterday(today)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(22,plain,
( ~ monday(yesterday(X0))
| tuesday(X0) ),
inference(cnf,[status(esa)],[monday_yesterday]) ).
cnf(l165,plain,
( ~ monday(yesterday(today))
| tuesday(today) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l264,plain,
( ~ tuesday(today)
| monday(yesterday(today)) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l321,plain,
( ~ member(today,lying_days(unicorn))
| thursday(today)
| friday(today)
| saturday(today) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l1461,plain,
admits(unicorn,today,yesterday(today)),
inference(instantiation,[status(thm)],[49]) ).
cnf(l1328,plain,
( ~ monday(yesterday(today))
| tuesday(today) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(33,plain,
( ~ saturday(X0)
| friday(yesterday(X0)) ),
inference(cnf,[status(esa)],[yesterday_friday]) ).
cnf(l1331,plain,
( ~ saturday(today)
| friday(yesterday(today)) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l388,plain,
( ~ tuesday(today)
| member(today,lying_days(lion)) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l1352,plain,
( ~ tuesday(yesterday(today))
| wednesday(today) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(10,plain,
( ~ tuesday(X0)
| ~ saturday(X0) ),
inference(cnf,[status(esa)],[tuesday_not_saturday]) ).
cnf(l152,plain,
( ~ tuesday(yesterday(today))
| ~ saturday(yesterday(today)) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l164,plain,
( ~ sunday(today)
| saturday(yesterday(today)) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l240,plain,
( ~ member(today,lying_days(lion))
| ~ member(yesterday(today),lying_days(lion))
| ~ admits(lion,today,yesterday(today)) ),
inference(instantiation,[status(thm)],[46]) ).
cnf(l1323,plain,
( ~ thursday(yesterday(today))
| friday(today) ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1334,plain,
( ~ tuesday(today)
| ~ saturday(today) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l266,plain,
( ~ saturday(yesterday(today))
| sunday(today) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l293,plain,
admits(lion,today,yesterday(today)),
inference(instantiation,[status(thm)],[48]) ).
cnf(18,plain,
( ~ thursday(X0)
| ~ sunday(X0) ),
inference(cnf,[status(esa)],[thursday_not_sunday]) ).
cnf(l1575,plain,
( ~ thursday(yesterday(today))
| ~ sunday(yesterday(today)) ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l2415,plain,
( ~ wednesday(today)
| ~ friday(today) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(11,plain,
( ~ tuesday(X0)
| ~ sunday(X0) ),
inference(cnf,[status(esa)],[tuesday_not_sunday]) ).
cnf(l294,plain,
( ~ tuesday(today)
| ~ sunday(today) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1586,plain,
( ~ monday(today)
| sunday(yesterday(today)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l2194,plain,
( ~ tuesday(today)
| member(today,lying_days(lion)) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l1277,plain,
( ~ monday(yesterday(today))
| ~ friday(yesterday(today)) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(20,plain,
( ~ friday(X0)
| ~ sunday(X0) ),
inference(cnf,[status(esa)],[friday_not_sunday]) ).
cnf(l2692,plain,
( ~ friday(yesterday(today))
| ~ sunday(yesterday(today)) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(28,plain,
( ~ sunday(yesterday(X0))
| monday(X0) ),
inference(cnf,[status(esa)],[sunday_yesterday]) ).
cnf(l1332,plain,
( ~ sunday(yesterday(today))
| monday(today) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l342,plain,
( ~ wednesday(yesterday(today))
| ~ saturday(yesterday(today)) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1506,plain,
( ~ monday(today)
| ~ saturday(today) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l2041,plain,
( ~ tuesday(today)
| monday(yesterday(today)) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(19,plain,
( ~ friday(X0)
| ~ saturday(X0) ),
inference(cnf,[status(esa)],[friday_not_saturday]) ).
cnf(l1343,plain,
( ~ friday(today)
| ~ saturday(today) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1353,plain,
( ~ wednesday(today)
| ~ saturday(today) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l2762,plain,
( ~ sunday(today)
| saturday(yesterday(today)) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(42,plain,
( ~ friday(X0)
| member(X0,lying_days(unicorn)) ),
inference(cnf,[status(esa)],[unicorn_lies_on_friday]) ).
cnf(l1330,plain,
( ~ friday(yesterday(today))
| member(yesterday(today),lying_days(unicorn)) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l2736,plain,
( ~ monday(today)
| sunday(yesterday(today)) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l91,l99,l98,l118,l90,l92,l96,l124,l93,l207,l125,l177,l2338,l102,l1211,l309,l126,l210,l230,l346,l100,l366,l345,l106,l128,l1450,l216,l2182,l108,l149,l127,l2682,l1313,l2056,l247,l308,l173,l2045,l265,l157,l295,l220,l158,l262,l2180,l1414,l1502,l256,l1574,l1316,l2746,l2120,l289,l1460,l2035,l150,l359,l236,l1329,l2763,l165,l264,l321,l1461,l1328,l1331,l388,l1352,l152,l164,l240,l1323,l1334,l266,l293,l1575,l2415,l294,l1586,l2194,l1277,l2692,l1332,l342,l1506,l2041,l1343,l1353,l2762,l1330,l2736]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : PUZ005-1 : TPTP v9.0.0. Released v1.0.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.34 % Computer : n017.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 : 300
% 0.13/0.34 % DateTime : Mon Jul 21 15:47:19 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.19/0.34 % launching worker at depth: 4
% 0.19/0.34 % launching worker at depth: 6
% 0.19/0.34 % launching worker at depth: 3
% 0.19/0.34 % launching worker at depth: 5
% 0.19/0.34 % launching worker at depth: 2
% 0.19/0.34 % launching worker at depth: 7
% 0.19/0.34 % launching worker at depth: 8
% 0.19/0.34 % launching worker at depth: 1
% 0.19/0.34 % launching worker at depth: 9
% 0.19/0.35 % launching worker at depth: 10
% 0.19/0.35 % launching worker at depth: 11
% 0.19/0.40 % launching worker at depth: 12
% 2.54/0.65 % launching worker at depth: 13
% 11.96/1.85 % launching worker at depth: 14
% 48.64/6.44 % SZS status Theorem for theBenchmark
% 48.64/6.44 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------