%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : MGT112+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n020.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 : Tue Sep 8 06:16:18 AM UTC 2026
% Result : Unsatisfiable 0.10s 0.37s
% Output : CNFRefutation 0.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 9
% Syntax : Number of formulae : 41 ( 27 unt; 0 def)
% Number of atoms : 111 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 149 ( 79 ~; 63 |; 6 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 50 ( 11 sgn 23 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax_disability_block,axiom,
! [F,X,Y,A,T] :
( ( proh(F)
& aee(F,X)
& aer(F,Y)
& act(F,A)
& tgt(F,T) )
=> ~ ? [Db] :
( disability(Db)
& bearer(Db,Y)
& cnt(Db,A,T) ) ) ).
fof(disability_db,axiom,
disability(db) ).
fof(bearer_db,axiom,
bearer(db,museen) ).
fof(cnt_db,axiom,
cnt(db,read,museum_api) ).
fof(proh_f2,axiom,
proh(f2) ).
fof(aee_f2,axiom,
aee(f2,bibliothek) ).
fof(aer_f2,axiom,
aer(f2,museen) ).
fof(act_f2,axiom,
act(f2,read) ).
fof(tgt_f2,axiom,
tgt(f2,museum_api) ).
fof(normalize_0_0,plain,
aee(f2,bibliothek),
inference(canonicalize,[],[aee_f2]) ).
fof(normalize_0_1,plain,
bearer(db,museen),
inference(canonicalize,[],[bearer_db]) ).
fof(normalize_0_2,plain,
tgt(f2,museum_api),
inference(canonicalize,[],[tgt_f2]) ).
fof(normalize_0_3,plain,
cnt(db,read,museum_api),
inference(canonicalize,[],[cnt_db]) ).
fof(normalize_0_4,plain,
! [A,F,T,X,Y] :
( ~ act(F,A)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ proh(F)
| ~ tgt(F,T)
| ! [Db] :
( ~ bearer(Db,Y)
| ~ cnt(Db,A,T)
| ~ disability(Db) ) ),
inference(canonicalize,[],[ax_disability_block]) ).
fof(normalize_0_5,plain,
! [A,F,T,X,Y] :
( ~ act(F,A)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ proh(F)
| ~ tgt(F,T)
| ! [Db] :
( ~ bearer(Db,Y)
| ~ cnt(Db,A,T)
| ~ disability(Db) ) ),
inference(specialize,[],[normalize_0_4]) ).
fof(normalize_0_6,plain,
! [A,Db,F,T,X,Y] :
( ~ act(F,A)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ bearer(Db,Y)
| ~ cnt(Db,A,T)
| ~ disability(Db)
| ~ proh(F)
| ~ tgt(F,T) ),
inference(clausify,[],[normalize_0_5]) ).
fof(normalize_0_7,plain,
disability(db),
inference(canonicalize,[],[disability_db]) ).
fof(normalize_0_8,plain,
act(f2,read),
inference(canonicalize,[],[act_f2]) ).
fof(normalize_0_9,plain,
proh(f2),
inference(canonicalize,[],[proh_f2]) ).
fof(normalize_0_10,plain,
aer(f2,museen),
inference(canonicalize,[],[aer_f2]) ).
cnf(refute_0_0,plain,
aee(f2,bibliothek),
inference(canonicalize,[],[normalize_0_0]) ).
cnf(refute_0_1,plain,
bearer(db,museen),
inference(canonicalize,[],[normalize_0_1]) ).
cnf(refute_0_2,plain,
tgt(f2,museum_api),
inference(canonicalize,[],[normalize_0_2]) ).
cnf(refute_0_3,plain,
cnt(db,read,museum_api),
inference(canonicalize,[],[normalize_0_3]) ).
cnf(refute_0_4,plain,
( ~ act(F,A)
| ~ aee(F,X)
| ~ aer(F,Y)
| ~ bearer(Db,Y)
| ~ cnt(Db,A,T)
| ~ disability(Db)
| ~ proh(F)
| ~ tgt(F,T) ),
inference(canonicalize,[],[normalize_0_6]) ).
cnf(refute_0_5,plain,
( ~ act(X_2,read)
| ~ aee(X_2,X_4)
| ~ aer(X_2,X_5)
| ~ bearer(db,X_5)
| ~ cnt(db,read,museum_api)
| ~ disability(db)
| ~ proh(X_2)
| ~ tgt(X_2,museum_api) ),
inference(subst,[],[refute_0_4:[bind(A,$fot(read)),bind(Db,$fot(db)),bind(F,$fot(X_2)),bind(T,$fot(museum_api)),bind(X,$fot(X_4)),bind(Y,$fot(X_5))]]) ).
cnf(refute_0_6,plain,
( ~ act(X_2,read)
| ~ aee(X_2,X_4)
| ~ aer(X_2,X_5)
| ~ bearer(db,X_5)
| ~ disability(db)
| ~ proh(X_2)
| ~ tgt(X_2,museum_api) ),
inference(resolve,[$cnf( cnt(db,read,museum_api) )],[refute_0_3,refute_0_5]) ).
cnf(refute_0_7,plain,
disability(db),
inference(canonicalize,[],[normalize_0_7]) ).
cnf(refute_0_8,plain,
( ~ act(X_2,read)
| ~ aee(X_2,X_4)
| ~ aer(X_2,X_5)
| ~ bearer(db,X_5)
| ~ proh(X_2)
| ~ tgt(X_2,museum_api) ),
inference(resolve,[$cnf( disability(db) )],[refute_0_7,refute_0_6]) ).
cnf(refute_0_9,plain,
( ~ act(f2,read)
| ~ aee(f2,X_7)
| ~ aer(f2,X_8)
| ~ bearer(db,X_8)
| ~ proh(f2)
| ~ tgt(f2,museum_api) ),
inference(subst,[],[refute_0_8:[bind(X_2,$fot(f2)),bind(X_4,$fot(X_7)),bind(X_5,$fot(X_8))]]) ).
cnf(refute_0_10,plain,
( ~ act(f2,read)
| ~ aee(f2,X_7)
| ~ aer(f2,X_8)
| ~ bearer(db,X_8)
| ~ proh(f2) ),
inference(resolve,[$cnf( tgt(f2,museum_api) )],[refute_0_2,refute_0_9]) ).
cnf(refute_0_11,plain,
act(f2,read),
inference(canonicalize,[],[normalize_0_8]) ).
cnf(refute_0_12,plain,
( ~ aee(f2,X_7)
| ~ aer(f2,X_8)
| ~ bearer(db,X_8)
| ~ proh(f2) ),
inference(resolve,[$cnf( act(f2,read) )],[refute_0_11,refute_0_10]) ).
cnf(refute_0_13,plain,
proh(f2),
inference(canonicalize,[],[normalize_0_9]) ).
cnf(refute_0_14,plain,
( ~ aee(f2,X_7)
| ~ aer(f2,X_8)
| ~ bearer(db,X_8) ),
inference(resolve,[$cnf( proh(f2) )],[refute_0_13,refute_0_12]) ).
cnf(refute_0_15,plain,
( ~ aee(f2,X_9)
| ~ aer(f2,museen)
| ~ bearer(db,museen) ),
inference(subst,[],[refute_0_14:[bind(X_7,$fot(X_9)),bind(X_8,$fot(museen))]]) ).
cnf(refute_0_16,plain,
( ~ aee(f2,X_9)
| ~ aer(f2,museen) ),
inference(resolve,[$cnf( bearer(db,museen) )],[refute_0_1,refute_0_15]) ).
cnf(refute_0_17,plain,
aer(f2,museen),
inference(canonicalize,[],[normalize_0_10]) ).
cnf(refute_0_18,plain,
~ aee(f2,X_9),
inference(resolve,[$cnf( aer(f2,museen) )],[refute_0_17,refute_0_16]) ).
cnf(refute_0_19,plain,
~ aee(f2,bibliothek),
inference(subst,[],[refute_0_18:[bind(X_9,$fot(bibliothek))]]) ).
cnf(refute_0_20,plain,
$false,
inference(resolve,[$cnf( aee(f2,bibliothek) )],[refute_0_0,refute_0_19]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT112+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.04 % Command : metis --show proof --show saturation %s
% 0.10/0.35 % Computer : n020.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 7 14:07:28 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.10/0.37 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37
% 0.10/0.37 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.10/0.37
%------------------------------------------------------------------------------