%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : MGT117+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 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 : Tue Sep 8 06:11:35 AM UTC 2026
% Result : Theorem 0.03s 0.30s
% Output : CNFRefutation 0.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 9
% Syntax : Number of formulae : 65 ( 50 unt; 0 def)
% Number of atoms : 166 ( 0 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 182 ( 81 ~; 78 |; 22 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 14 ( 13 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-6 aty)
% Number of variables : 45 ( 0 sgn 6 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(conjecture,plain,
? [RhoI,Db] :
( founds_imm(e1,RhoI,p1)
& disability(Db)
& bearer(Db,museen)
& cnt(Db,read,museum_api)
& part_of(Db,RhoI) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture) ).
fof(conjecture_negated,plain,
~ ? [RhoI,Db] :
( founds_imm(e1,RhoI,p1)
& disability(Db)
& bearer(Db,museen)
& cnt(Db,read,museum_api)
& part_of(Db,RhoI) ),
inference(negate_conjecture,[status(cth)],[conjecture]) ).
cnf(22,plain,
( ~ bearer(X0,museen)
| ~ cnt(X0,read,museum_api)
| ~ part_of(X0,X1)
| ~ disability(X0)
| ~ founds_imm(e1,X1,p1) ),
inference(cnf,[status(esa)],[conjecture_negated]) ).
cnf(l0,plain,
( ~ bearer(sK3(p1,bibliothek,museen,read,museum_api,e1),museen)
| ~ cnt(sK3(p1,bibliothek,museen,read,museum_api,e1),read,museum_api)
| ~ part_of(sK3(p1,bibliothek,museen,read,museum_api,e1),sK1(p1,bibliothek,museen,read,museum_api,e1))
| ~ disability(sK3(p1,bibliothek,museen,read,museum_api,e1))
| ~ founds_imm(e1,sK1(p1,bibliothek,museen,read,museum_api,e1),p1) ),
inference(instantiation,[status(thm)],[22]) ).
fof(ax_perm_relator_strong,plain,
! [P,X,Y,A,T,E] :
( ( perm(P)
& strong(P)
& aee(P,X)
& aer(P,Y)
& act(P,A)
& tgt(P,T)
& activates(E,P) )
=> ? [RhoI,Im,Db] :
( founds_imm(E,RhoI,P)
& immunity(Im)
& bearer(Im,X)
& cnt(Im,A,T)
& part_of(Im,RhoI)
& disability(Db)
& bearer(Db,Y)
& cnt(Db,A,T)
& part_of(Db,RhoI) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_perm_relator_strong) ).
cnf(7,plain,
( ~ perm(X0)
| ~ aer(X0,X1)
| ~ act(X0,X2)
| ~ tgt(X0,X3)
| ~ strong(X0)
| ~ aee(X0,X4)
| ~ activates(X5,X0)
| cnt(sK3(X0,X4,X1,X2,X3,X5),X2,X3) ),
inference(cnf,[status(esa)],[ax_perm_relator_strong]) ).
cnf(l1,plain,
( ~ perm(p1)
| ~ aer(p1,museen)
| ~ act(p1,read)
| ~ tgt(p1,museum_api)
| ~ strong(p1)
| ~ aee(p1,bibliothek)
| ~ activates(e1,p1)
| cnt(sK3(p1,bibliothek,museen,read,museum_api,e1),read,museum_api) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(6,plain,
( ~ perm(X0)
| ~ aer(X0,X1)
| ~ act(X0,X2)
| ~ tgt(X0,X3)
| ~ strong(X0)
| ~ aee(X0,X4)
| ~ activates(X5,X0)
| bearer(sK3(X0,X4,X1,X2,X3,X5),X1) ),
inference(cnf,[status(esa)],[ax_perm_relator_strong]) ).
cnf(l2,plain,
( ~ perm(p1)
| ~ aer(p1,museen)
| ~ act(p1,read)
| ~ tgt(p1,museum_api)
| ~ strong(p1)
| ~ aee(p1,bibliothek)
| ~ activates(e1,p1)
| bearer(sK3(p1,bibliothek,museen,read,museum_api,e1),museen) ),
inference(instantiation,[status(thm)],[6]) ).
fof(aer_p1,plain,
aer(p1,museen),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aer_p1) ).
cnf(18,plain,
aer(p1,museen),
inference(cnf,[status(esa)],[aer_p1]) ).
cnf(l3,plain,
aer(p1,museen),
inference(instantiation,[status(thm)],[18]) ).
fof(act_e1_p1,plain,
activates(e1,p1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',act_e1_p1) ).
cnf(21,plain,
activates(e1,p1),
inference(cnf,[status(esa)],[act_e1_p1]) ).
cnf(l4,plain,
activates(e1,p1),
inference(instantiation,[status(thm)],[21]) ).
cnf(0,plain,
( ~ perm(X0)
| ~ aer(X0,X1)
| ~ act(X0,X2)
| ~ tgt(X0,X3)
| ~ strong(X0)
| ~ aee(X0,X4)
| ~ activates(X5,X0)
| founds_imm(X5,sK1(X0,X4,X1,X2,X3,X5),X0) ),
inference(cnf,[status(esa)],[ax_perm_relator_strong]) ).
cnf(l5,plain,
( ~ perm(p1)
| ~ aer(p1,museen)
| ~ act(p1,read)
| ~ tgt(p1,museum_api)
| ~ strong(p1)
| ~ aee(p1,bibliothek)
| ~ activates(e1,p1)
| founds_imm(e1,sK1(p1,bibliothek,museen,read,museum_api,e1),p1) ),
inference(instantiation,[status(thm)],[0]) ).
fof(strong_p1,plain,
strong(p1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',strong_p1) ).
cnf(16,plain,
strong(p1),
inference(cnf,[status(esa)],[strong_p1]) ).
cnf(l6,plain,
strong(p1),
inference(instantiation,[status(thm)],[16]) ).
fof(act_p1,plain,
act(p1,read),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',act_p1) ).
cnf(19,plain,
act(p1,read),
inference(cnf,[status(esa)],[act_p1]) ).
cnf(l7,plain,
act(p1,read),
inference(instantiation,[status(thm)],[19]) ).
cnf(l8,plain,
act(p1,read),
inference(instantiation,[status(thm)],[19]) ).
fof(perm_p1,plain,
perm(p1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',perm_p1) ).
cnf(15,plain,
perm(p1),
inference(cnf,[status(esa)],[perm_p1]) ).
cnf(l9,plain,
perm(p1),
inference(instantiation,[status(thm)],[15]) ).
cnf(l10,plain,
activates(e1,p1),
inference(instantiation,[status(thm)],[21]) ).
cnf(l11,plain,
strong(p1),
inference(instantiation,[status(thm)],[16]) ).
cnf(8,plain,
( ~ perm(X0)
| ~ aer(X0,X1)
| ~ act(X0,X2)
| ~ tgt(X0,X3)
| ~ strong(X0)
| ~ aee(X0,X4)
| ~ activates(X5,X0)
| part_of(sK3(X0,X4,X1,X2,X3,X5),sK1(X0,X4,X1,X2,X3,X5)) ),
inference(cnf,[status(esa)],[ax_perm_relator_strong]) ).
cnf(l12,plain,
( ~ perm(p1)
| ~ aer(p1,museen)
| ~ act(p1,read)
| ~ tgt(p1,museum_api)
| ~ strong(p1)
| ~ aee(p1,bibliothek)
| ~ activates(e1,p1)
| part_of(sK3(p1,bibliothek,museen,read,museum_api,e1),sK1(p1,bibliothek,museen,read,museum_api,e1)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l13,plain,
act(p1,read),
inference(instantiation,[status(thm)],[19]) ).
fof(tgt_p1,plain,
tgt(p1,museum_api),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tgt_p1) ).
cnf(20,plain,
tgt(p1,museum_api),
inference(cnf,[status(esa)],[tgt_p1]) ).
cnf(l14,plain,
tgt(p1,museum_api),
inference(instantiation,[status(thm)],[20]) ).
cnf(l15,plain,
act(p1,read),
inference(instantiation,[status(thm)],[19]) ).
cnf(5,plain,
( ~ perm(X0)
| ~ aer(X0,X1)
| ~ act(X0,X2)
| ~ tgt(X0,X3)
| ~ strong(X0)
| ~ aee(X0,X4)
| ~ activates(X5,X0)
| disability(sK3(X0,X4,X1,X2,X3,X5)) ),
inference(cnf,[status(esa)],[ax_perm_relator_strong]) ).
cnf(l16,plain,
( ~ perm(p1)
| ~ aer(p1,museen)
| ~ act(p1,read)
| ~ tgt(p1,museum_api)
| ~ strong(p1)
| ~ aee(p1,bibliothek)
| ~ activates(e1,p1)
| disability(sK3(p1,bibliothek,museen,read,museum_api,e1)) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l17,plain,
tgt(p1,museum_api),
inference(instantiation,[status(thm)],[20]) ).
cnf(l18,plain,
tgt(p1,museum_api),
inference(instantiation,[status(thm)],[20]) ).
cnf(l19,plain,
aer(p1,museen),
inference(instantiation,[status(thm)],[18]) ).
cnf(l20,plain,
activates(e1,p1),
inference(instantiation,[status(thm)],[21]) ).
cnf(l21,plain,
activates(e1,p1),
inference(instantiation,[status(thm)],[21]) ).
cnf(l22,plain,
act(p1,read),
inference(instantiation,[status(thm)],[19]) ).
fof(aee_p1,plain,
aee(p1,bibliothek),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aee_p1) ).
cnf(17,plain,
aee(p1,bibliothek),
inference(cnf,[status(esa)],[aee_p1]) ).
cnf(l23,plain,
aee(p1,bibliothek),
inference(instantiation,[status(thm)],[17]) ).
cnf(l24,plain,
strong(p1),
inference(instantiation,[status(thm)],[16]) ).
cnf(l25,plain,
perm(p1),
inference(instantiation,[status(thm)],[15]) ).
cnf(l26,plain,
aer(p1,museen),
inference(instantiation,[status(thm)],[18]) ).
cnf(l27,plain,
strong(p1),
inference(instantiation,[status(thm)],[16]) ).
cnf(l28,plain,
strong(p1),
inference(instantiation,[status(thm)],[16]) ).
cnf(l29,plain,
aee(p1,bibliothek),
inference(instantiation,[status(thm)],[17]) ).
cnf(l30,plain,
aee(p1,bibliothek),
inference(instantiation,[status(thm)],[17]) ).
cnf(l31,plain,
perm(p1),
inference(instantiation,[status(thm)],[15]) ).
cnf(l32,plain,
aer(p1,museen),
inference(instantiation,[status(thm)],[18]) ).
cnf(l33,plain,
perm(p1),
inference(instantiation,[status(thm)],[15]) ).
cnf(l34,plain,
tgt(p1,museum_api),
inference(instantiation,[status(thm)],[20]) ).
cnf(l35,plain,
aer(p1,museen),
inference(instantiation,[status(thm)],[18]) ).
cnf(l36,plain,
aee(p1,bibliothek),
inference(instantiation,[status(thm)],[17]) ).
cnf(l37,plain,
aee(p1,bibliothek),
inference(instantiation,[status(thm)],[17]) ).
cnf(l38,plain,
perm(p1),
inference(instantiation,[status(thm)],[15]) ).
cnf(l39,plain,
activates(e1,p1),
inference(instantiation,[status(thm)],[21]) ).
cnf(l40,plain,
tgt(p1,museum_api),
inference(instantiation,[status(thm)],[20]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l3,l4,l5,l6,l7,l8,l9,l10,l11,l12,l13,l14,l15,l16,l17,l18,l19,l20,l21,l22,l23,l24,l25,l26,l27,l28,l29,l30,l31,l32,l33,l34,l35,l36,l37,l38,l39,l40]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : MGT117+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.02 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Mon Sep 7 14:09:41 UTC 2026
% 0.03/0.29 % CPUTime :
% 0.03/0.30 % launching worker at depth: 1
% 0.03/0.30 % launching worker at depth: 2
% 0.03/0.30 % launching worker at depth: 8
% 0.03/0.30 % launching worker at depth: 4
% 0.03/0.30 % launching worker at depth: 5
% 0.03/0.30 % launching worker at depth: 6
% 0.03/0.30 % launching worker at depth: 7
% 0.03/0.30 % launching worker at depth: 3
% 0.03/0.30 % launching worker at depth: 9
% 0.03/0.30 % SZS status Theorem for theBenchmark
% 0.03/0.30 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------