%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : PUZ005-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n012.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:32:39 PM UTC 2026
% Result : Unsatisfiable 0.18s 0.97s
% Output : CNFRefutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 21
% Syntax : Number of formulae : 68 ( 8 unt; 0 def)
% Number of atoms : 147 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 155 ( 76 ~; 79 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 10 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-1 aty)
% Number of variables : 47 ( 0 sgn 47 !; 0 ?; 25 :)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [X0] :
( ~ saturday(X0)
| ~ monday(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',monday_not_saturday) ).
fof(f11,axiom,
! [X0] :
( ~ saturday(X0)
| ~ tuesday(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tuesday_not_saturday) ).
fof(f22,axiom,
! [X0] :
( ~ sunday(X0)
| ~ saturday(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',saturday_not_sunday) ).
fof(f25,axiom,
! [X0] :
( thursday(X0)
| ~ wednesday(yesterday(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wednesday_yesterday) ).
fof(f26,axiom,
! [X0] :
( friday(X0)
| ~ thursday(yesterday(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thursday_yesterday) ).
fof(f27,axiom,
! [X0] :
( saturday(X0)
| ~ friday(yesterday(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',friday_yesterday) ).
fof(f30,axiom,
! [X0] :
( ~ tuesday(X0)
| monday(yesterday(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',yesterday_monday) ).
fof(f31,axiom,
! [X0] :
( ~ wednesday(X0)
| tuesday(yesterday(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',yesterday_tuesday) ).
fof(f33,axiom,
! [X0] :
( ~ friday(X0)
| thursday(yesterday(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',yesterday_thursday) ).
fof(f34,axiom,
! [X0] :
( ~ saturday(X0)
| friday(yesterday(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',yesterday_friday) ).
fof(f36,axiom,
! [X0] :
( ~ monday(X0)
| sunday(yesterday(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',yesterday_sunday) ).
fof(f37,axiom,
! [X0] :
( wednesday(X0)
| tuesday(X0)
| monday(X0)
| ~ member(X0,lying_days(lion)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lions_lying_days) ).
fof(f38,axiom,
! [X0] :
( saturday(X0)
| friday(X0)
| thursday(X0)
| ~ member(X0,lying_days(unicorn)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unicorns_lying_days) ).
fof(f42,axiom,
! [X0] :
( member(X0,lying_days(unicorn))
| ~ thursday(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unicorn_lies_on_thursday) ).
fof(f43,axiom,
! [X0] :
( member(X0,lying_days(unicorn))
| ~ friday(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unicorn_lies_on_friday) ).
fof(f44,axiom,
! [X0] :
( member(X0,lying_days(unicorn))
| ~ saturday(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unicorn_lies_on_saturday) ).
fof(f45,axiom,
! [X2,X0,X1] :
( member(X2,lying_days(X1))
| ~ admits(X1,X0,X2)
| member(X0,lying_days(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',admissions1) ).
fof(f47,axiom,
! [X2,X0,X1] :
( ~ member(X2,lying_days(X1))
| ~ admits(X1,X0,X2)
| ~ member(X0,lying_days(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',admissions3) ).
fof(f49,axiom,
admits(lion,today,yesterday(today)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',admissions5) ).
fof(f50,axiom,
admits(unicorn,today,yesterday(today)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',admissions6) ).
fof(f51,negated_conjecture,
~ thursday(today),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_today_is_thursday) ).
tcf(c_105,plain,
! [X0: $i] :
( ~ saturday(X0)
| ~ monday(X0) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_110,plain,
! [X0: $i] :
( ~ saturday(X0)
| ~ tuesday(X0) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_121,plain,
! [X0: $i] :
( ~ sunday(X0)
| ~ saturday(X0) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_124,plain,
! [X0: $i] :
( thursday(X0)
| ~ wednesday(yesterday(X0)) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_125,plain,
! [X0: $i] :
( friday(X0)
| ~ thursday(yesterday(X0)) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_126,plain,
! [X0: $i] :
( saturday(X0)
| ~ friday(yesterday(X0)) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_129,plain,
! [X0: $i] :
( monday(yesterday(X0))
| ~ tuesday(X0) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_130,plain,
! [X0: $i] :
( tuesday(yesterday(X0))
| ~ wednesday(X0) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_132,plain,
! [X0: $i] :
( thursday(yesterday(X0))
| ~ friday(X0) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_133,plain,
! [X0: $i] :
( friday(yesterday(X0))
| ~ saturday(X0) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_135,plain,
! [X0: $i] :
( sunday(yesterday(X0))
| ~ monday(X0) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_136,plain,
! [X0: $i] :
( wednesday(X0)
| tuesday(X0)
| monday(X0)
| ~ member(X0,lying_days(lion)) ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_137,plain,
! [X0: $i] :
( saturday(X0)
| friday(X0)
| thursday(X0)
| ~ member(X0,lying_days(unicorn)) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_141,plain,
! [X0: $i] :
( member(X0,lying_days(unicorn))
| ~ thursday(X0) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_142,plain,
! [X0: $i] :
( member(X0,lying_days(unicorn))
| ~ friday(X0) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_143,plain,
! [X0: $i] :
( member(X0,lying_days(unicorn))
| ~ saturday(X0) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_144,plain,
! [X0: $i,X1: $i,X2: $i] :
( member(X2,lying_days(X0))
| member(X1,lying_days(X0))
| ~ admits(X0,X1,X2) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_146,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ member(X2,lying_days(X0))
| ~ member(X1,lying_days(X0))
| ~ admits(X0,X1,X2) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_148,plain,
admits(lion,today,yesterday(today)),
inference(cnf_transformation,[],[f49]) ).
tcf(c_149,plain,
admits(unicorn,today,yesterday(today)),
inference(cnf_transformation,[],[f50]) ).
tcf(c_150,negated_conjecture,
~ thursday(today),
inference(cnf_transformation,[],[f51]) ).
tcf(c_205,plain,
! [X0: $i] :
( ~ wednesday(yesterday(X0))
| thursday(X0) ),
inference(prop_impl_just,[status(thm)],[c_124]) ).
tcf(c_206,plain,
! [X0: $i] :
( thursday(X0)
| ~ wednesday(yesterday(X0)) ),
inference(renaming,[status(thm)],[c_205]) ).
tcf(c_626,plain,
( member(today,lying_days(lion))
| member(yesterday(today),lying_days(lion)) ),
inference(resolution,[status(thm)],[c_144,c_148]) ).
tcf(c_633,plain,
( ~ member(today,lying_days(unicorn))
| ~ member(yesterday(today),lying_days(unicorn)) ),
inference(resolution,[status(thm)],[c_146,c_149]) ).
tcf(c_640,plain,
( member(today,lying_days(unicorn))
| member(yesterday(today),lying_days(unicorn)) ),
inference(resolution,[status(thm)],[c_144,c_149]) ).
tcf(c_2740,plain,
( saturday(today)
| friday(today)
| ~ member(today,lying_days(unicorn)) ),
inference(resolution,[status(thm)],[c_137,c_150]) ).
tcf(c_2750,plain,
~ wednesday(yesterday(today)),
inference(resolution,[status(thm)],[c_206,c_150]) ).
tcf(c_5327,plain,
( saturday(yesterday(today))
| friday(yesterday(today))
| thursday(yesterday(today))
| ~ member(yesterday(today),lying_days(unicorn)) ),
inference(instantiation,[status(thm)],[c_137]) ).
tcf(c_5333,plain,
! [X0: $i] :
( ~ sunday(yesterday(X0))
| ~ saturday(yesterday(X0)) ),
inference(instantiation,[status(thm)],[c_121]) ).
tcf(c_5338,plain,
( wednesday(yesterday(today))
| tuesday(yesterday(today))
| monday(yesterday(today))
| ~ member(yesterday(today),lying_days(lion)) ),
inference(instantiation,[status(thm)],[c_136]) ).
tcf(c_5339,plain,
( member(yesterday(today),lying_days(unicorn))
| ~ thursday(yesterday(today)) ),
inference(instantiation,[status(thm)],[c_141]) ).
tcf(c_5344,plain,
( friday(today)
| ~ thursday(yesterday(today)) ),
inference(instantiation,[status(thm)],[c_125]) ).
tcf(c_5348,plain,
( ~ saturday(yesterday(today))
| ~ monday(yesterday(today)) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_5384,plain,
( member(today,lying_days(unicorn))
| ~ friday(today) ),
inference(instantiation,[status(thm)],[c_142]) ).
tcf(c_5387,plain,
( thursday(yesterday(today))
| ~ friday(today) ),
inference(instantiation,[status(thm)],[c_132]) ).
tcf(c_5432,plain,
( member(today,lying_days(unicorn))
| ~ saturday(today) ),
inference(instantiation,[status(thm)],[c_143]) ).
tcf(c_5433,plain,
( friday(yesterday(today))
| ~ saturday(today) ),
inference(instantiation,[status(thm)],[c_133]) ).
tcf(c_5450,plain,
( monday(yesterday(today))
| ~ tuesday(today) ),
inference(instantiation,[status(thm)],[c_129]) ).
tcf(c_5471,plain,
( member(yesterday(today),lying_days(unicorn))
| ~ friday(yesterday(today)) ),
inference(instantiation,[status(thm)],[c_142]) ).
tcf(c_5475,plain,
( saturday(today)
| ~ friday(yesterday(today)) ),
inference(instantiation,[status(thm)],[c_126]) ).
tcf(c_5501,plain,
( tuesday(yesterday(today))
| ~ wednesday(today) ),
inference(instantiation,[status(thm)],[c_130]) ).
tcf(c_5546,plain,
( ~ saturday(yesterday(today))
| ~ tuesday(yesterday(today)) ),
inference(instantiation,[status(thm)],[c_110]) ).
tcf(c_5552,plain,
( ~ sunday(yesterday(today))
| ~ saturday(yesterday(today)) ),
inference(instantiation,[status(thm)],[c_5333]) ).
tcf(c_5592,plain,
( wednesday(today)
| tuesday(today)
| monday(today)
| ~ member(today,lying_days(lion)) ),
inference(instantiation,[status(thm)],[c_136]) ).
tcf(c_5639,plain,
( sunday(yesterday(today))
| ~ monday(today) ),
inference(instantiation,[status(thm)],[c_135]) ).
tcf(c_5646,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_5639,c_5592,c_5552,c_5546,c_5501,c_5475,c_5471,c_5450,c_5432,c_5433,c_5384,c_5387,c_5348,c_5344,c_5339,c_5338,c_5327,c_2750,c_2740,c_640,c_633,c_626]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : PUZ005-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.03/0.31 % Computer : n012.cluster.edu
% 0.03/0.31 % Model : x86_64 x86_64
% 0.03/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.31 % Memory : 8046.5625MB
% 0.03/0.31 % OS : Linux 6.8.0-71-generic
% 0.03/0.31 % CPULimit : 300
% 0.03/0.31 % WCLimit : 300
% 0.03/0.31 % DateTime : Thu Sep 24 06:36:06 UTC 2026
% 0.03/0.31 % CPUTime :
% 0.03/0.31 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.07/0.33 Running first-order theorem proving
% 0.07/0.33 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34
% 0.07/0.34 % ======== iProver multi-core TPTP/SMT =========
% 0.07/0.34
% 0.07/0.34 % Detected problem language: tptp
% 0.07/0.34 % Proving...
% 0.18/0.97 % SZS status Started for theBenchmark.p
% 0.18/0.97 % SZS status Unsatisfiable for theBenchmark.p
% 0.18/0.97
% 0.18/0.97 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 0.18/0.97
% 0.18/0.97 % ------ iProver source info
% 0.18/0.97
% 0.18/0.97 % git: date: 2026-07-19 20:42:38 +0200
% 0.18/0.97 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 0.18/0.97 % git: non_committed_changes: false
% 0.18/0.97
% 0.18/0.97 % ------ Parsing...% successful
% 0.18/0.97
% 0.18/0.97
% 0.18/0.97 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 0.18/0.97
% 0.18/0.97 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe:1:0s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 0.18/0.97
% 0.18/0.97 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 0.18/0.97 % ------ Proving...
% 0.18/0.97 % ------ Problem Properties
% 0.18/0.97
% 0.18/0.97 %
% 0.18/0.97 % clauses 49
% 0.18/0.97 % conjectures 1
% 0.18/0.97 % EPR 23
% 0.18/0.97 % Horn 44
% 0.18/0.97 % unary 1
% 0.18/0.97 % binary 45
% 0.18/0.97 % lits 106
% 0.18/0.97 % lits eq 0
% 0.18/0.97 % fd_pure 0
% 0.18/0.97 % fd_pseudo 0
% 0.18/0.97 % fd_cond 0
% 0.18/0.97 % fd_pseudo_cond 0
% 0.18/0.97 % AC symbols 0
% 0.18/0.97
% 0.18/0.97 % ------ Schedule dynamic 5 is on
% 0.18/0.97
% 0.18/0.97 % ------ no equalities: superposition off
% 0.18/0.97
% 0.18/0.97 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 0.18/0.97
% 0.18/0.97
% 0.18/0.97 % ------
% 0.18/0.97 % Current options:
% 0.18/0.97 % ------
% 0.18/0.97
% 0.18/0.97
% 0.18/0.97 %
% 0.18/0.97
% 0.18/0.97 % ------ Proving...
% 0.18/0.97 %
% 0.18/0.97
% 0.18/0.97 % SZS status Unsatisfiable for theBenchmark.p
% 0.18/0.97
% 0.18/0.97 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 0.18/0.97
% 0.18/0.97
%------------------------------------------------------------------------------