%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT117+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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:18:53 AM UTC 2026
% Result : Theorem 0.39s 0.66s
% Output : CNFRefutation 0.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 9
% Syntax : Number of formulae : 69 ( 21 unt; 0 def)
% Number of atoms : 366 ( 0 equ)
% Maximal formula atoms : 72 ( 5 avg)
% Number of connectives : 547 ( 250 ~; 242 |; 54 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 14 ( 13 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-6 aty)
% Number of variables : 130 ( 0 sgn 34 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(perm_p1,axiom,
perm(p1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',perm_p1) ).
cnf(c10,plain,
perm(p1),
inference(split_conjunct,[status(thm)],[perm_p1]) ).
fof(strong_p1,axiom,
strong(p1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',strong_p1) ).
cnf(c9,plain,
strong(p1),
inference(split_conjunct,[status(thm)],[strong_p1]) ).
fof(aee_p1,axiom,
aee(p1,bibliothek),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aee_p1) ).
cnf(c8,plain,
aee(p1,bibliothek),
inference(split_conjunct,[status(thm)],[aee_p1]) ).
fof(aer_p1,axiom,
aer(p1,museen),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aer_p1) ).
cnf(c7,plain,
aer(p1,museen),
inference(split_conjunct,[status(thm)],[aer_p1]) ).
fof(act_p1,axiom,
act(p1,read),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act_p1) ).
cnf(c6,plain,
act(p1,read),
inference(split_conjunct,[status(thm)],[act_p1]) ).
fof(tgt_p1,axiom,
tgt(p1,museum_api),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tgt_p1) ).
cnf(c5,plain,
tgt(p1,museum_api),
inference(split_conjunct,[status(thm)],[tgt_p1]) ).
fof(act_e1_p1,axiom,
activates(e1,p1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',act_e1_p1) ).
cnf(c4,plain,
activates(e1,p1),
inference(split_conjunct,[status(thm)],[act_e1_p1]) ).
fof(ax_perm_relator_strong,axiom,
! [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/sandbox/benchmark/theBenchmark.p',ax_perm_relator_strong) ).
fof(c17,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) ) ),
inference(fof_nnf,[status(thm)],[ax_perm_relator_strong]) ).
fof(c18,plain,
! [X4,X5,X6,X7,X8,X9] :
( ~ perm(X4)
| ~ strong(X4)
| ~ aee(X4,X5)
| ~ aer(X4,X6)
| ~ act(X4,X7)
| ~ tgt(X4,X8)
| ~ activates(X9,X4)
| ? [X10,X11,X12] :
( founds_imm(X9,X10,X4)
& immunity(X11)
& bearer(X11,X5)
& cnt(X11,X7,X8)
& part_of(X11,X10)
& disability(X12)
& bearer(X12,X6)
& cnt(X12,X7,X8)
& part_of(X12,X10) ) ),
inference(variable_rename,[status(thm)],[c17]) ).
fof(c19,plain,
! [X4,X5,X6,X7,X8,X9] :
( ~ perm(X4)
| ~ strong(X4)
| ~ aee(X4,X5)
| ~ aer(X4,X6)
| ~ act(X4,X7)
| ~ tgt(X4,X8)
| ~ activates(X9,X4)
| ( founds_imm(X9,skolem0001(X4,X5,X6,X7,X8,X9),X4)
& immunity(skolem0002(X4,X5,X6,X7,X8,X9))
& bearer(skolem0002(X4,X5,X6,X7,X8,X9),X5)
& cnt(skolem0002(X4,X5,X6,X7,X8,X9),X7,X8)
& part_of(skolem0002(X4,X5,X6,X7,X8,X9),skolem0001(X4,X5,X6,X7,X8,X9))
& disability(skolem0003(X4,X5,X6,X7,X8,X9))
& bearer(skolem0003(X4,X5,X6,X7,X8,X9),X6)
& cnt(skolem0003(X4,X5,X6,X7,X8,X9),X7,X8)
& part_of(skolem0003(X4,X5,X6,X7,X8,X9),skolem0001(X4,X5,X6,X7,X8,X9)) ) ),
inference(skolemize,[status(esa)],[c18]) ).
fof(c20,plain,
! [X4,X5,X6,X7,X8,X9] :
( ( ~ perm(X4)
| ~ strong(X4)
| ~ aee(X4,X5)
| ~ aer(X4,X6)
| ~ act(X4,X7)
| ~ tgt(X4,X8)
| ~ activates(X9,X4)
| founds_imm(X9,skolem0001(X4,X5,X6,X7,X8,X9),X4) )
& ( ~ perm(X4)
| ~ strong(X4)
| ~ aee(X4,X5)
| ~ aer(X4,X6)
| ~ act(X4,X7)
| ~ tgt(X4,X8)
| ~ activates(X9,X4)
| immunity(skolem0002(X4,X5,X6,X7,X8,X9)) )
& ( ~ perm(X4)
| ~ strong(X4)
| ~ aee(X4,X5)
| ~ aer(X4,X6)
| ~ act(X4,X7)
| ~ tgt(X4,X8)
| ~ activates(X9,X4)
| bearer(skolem0002(X4,X5,X6,X7,X8,X9),X5) )
& ( ~ perm(X4)
| ~ strong(X4)
| ~ aee(X4,X5)
| ~ aer(X4,X6)
| ~ act(X4,X7)
| ~ tgt(X4,X8)
| ~ activates(X9,X4)
| cnt(skolem0002(X4,X5,X6,X7,X8,X9),X7,X8) )
& ( ~ perm(X4)
| ~ strong(X4)
| ~ aee(X4,X5)
| ~ aer(X4,X6)
| ~ act(X4,X7)
| ~ tgt(X4,X8)
| ~ activates(X9,X4)
| part_of(skolem0002(X4,X5,X6,X7,X8,X9),skolem0001(X4,X5,X6,X7,X8,X9)) )
& ( ~ perm(X4)
| ~ strong(X4)
| ~ aee(X4,X5)
| ~ aer(X4,X6)
| ~ act(X4,X7)
| ~ tgt(X4,X8)
| ~ activates(X9,X4)
| disability(skolem0003(X4,X5,X6,X7,X8,X9)) )
& ( ~ perm(X4)
| ~ strong(X4)
| ~ aee(X4,X5)
| ~ aer(X4,X6)
| ~ act(X4,X7)
| ~ tgt(X4,X8)
| ~ activates(X9,X4)
| bearer(skolem0003(X4,X5,X6,X7,X8,X9),X6) )
& ( ~ perm(X4)
| ~ strong(X4)
| ~ aee(X4,X5)
| ~ aer(X4,X6)
| ~ act(X4,X7)
| ~ tgt(X4,X8)
| ~ activates(X9,X4)
| cnt(skolem0003(X4,X5,X6,X7,X8,X9),X7,X8) )
& ( ~ perm(X4)
| ~ strong(X4)
| ~ aee(X4,X5)
| ~ aer(X4,X6)
| ~ act(X4,X7)
| ~ tgt(X4,X8)
| ~ activates(X9,X4)
| part_of(skolem0003(X4,X5,X6,X7,X8,X9),skolem0001(X4,X5,X6,X7,X8,X9)) ) ),
inference(distribute,[status(thm)],[c19]) ).
cnf(c26,plain,
( ~ perm(X23)
| ~ strong(X23)
| ~ aee(X23,X25)
| ~ aer(X23,X24)
| ~ act(X23,X22)
| ~ tgt(X23,X26)
| ~ activates(X21,X23)
| disability(skolem0003(X23,X25,X24,X22,X26,X21)) ),
inference(split_conjunct,[status(thm)],[c20]) ).
cnf(c31,plain,
( ~ perm(p1)
| ~ strong(p1)
| ~ aee(p1,X80)
| ~ aer(p1,X82)
| ~ act(p1,X81)
| ~ tgt(p1,X79)
| disability(skolem0003(p1,X80,X82,X81,X79,e1)) ),
inference(resolution,[status(thm)],[c26,c4]) ).
cnf(c45,plain,
( ~ perm(p1)
| ~ strong(p1)
| ~ aee(p1,X84)
| ~ aer(p1,X85)
| ~ act(p1,X83)
| disability(skolem0003(p1,X84,X85,X83,museum_api,e1)) ),
inference(resolution,[status(thm)],[c31,c5]) ).
cnf(c46,plain,
( ~ perm(p1)
| ~ strong(p1)
| ~ aee(p1,X87)
| ~ aer(p1,X86)
| disability(skolem0003(p1,X87,X86,read,museum_api,e1)) ),
inference(resolution,[status(thm)],[c45,c6]) ).
cnf(c47,plain,
( ~ perm(p1)
| ~ strong(p1)
| ~ aee(p1,X88)
| disability(skolem0003(p1,X88,museen,read,museum_api,e1)) ),
inference(resolution,[status(thm)],[c46,c7]) ).
cnf(c48,plain,
( ~ perm(p1)
| ~ strong(p1)
| disability(skolem0003(p1,bibliothek,museen,read,museum_api,e1)) ),
inference(resolution,[status(thm)],[c47,c8]) ).
cnf(c49,plain,
( ~ perm(p1)
| disability(skolem0003(p1,bibliothek,museen,read,museum_api,e1)) ),
inference(resolution,[status(thm)],[c48,c9]) ).
cnf(c51,plain,
disability(skolem0003(p1,bibliothek,museen,read,museum_api,e1)),
inference(resolution,[status(thm)],[c49,c10]) ).
cnf(c27,plain,
( ~ perm(X41)
| ~ strong(X41)
| ~ aee(X41,X43)
| ~ aer(X41,X42)
| ~ act(X41,X40)
| ~ tgt(X41,X44)
| ~ activates(X39,X41)
| bearer(skolem0003(X41,X43,X42,X40,X44,X39),X42) ),
inference(split_conjunct,[status(thm)],[c20]) ).
cnf(c34,plain,
( ~ perm(p1)
| ~ strong(p1)
| ~ aee(p1,X109)
| ~ aer(p1,X110)
| ~ act(p1,X108)
| ~ tgt(p1,X111)
| bearer(skolem0003(p1,X109,X110,X108,X111,e1),X110) ),
inference(resolution,[status(thm)],[c27,c4]) ).
cnf(c60,plain,
( ~ perm(p1)
| ~ strong(p1)
| ~ aee(p1,X114)
| ~ aer(p1,X115)
| ~ act(p1,X113)
| bearer(skolem0003(p1,X114,X115,X113,museum_api,e1),X115) ),
inference(resolution,[status(thm)],[c34,c5]) ).
cnf(c64,plain,
( ~ perm(p1)
| ~ strong(p1)
| ~ aee(p1,X120)
| ~ aer(p1,X121)
| bearer(skolem0003(p1,X120,X121,read,museum_api,e1),X121) ),
inference(resolution,[status(thm)],[c60,c6]) ).
cnf(c66,plain,
( ~ perm(p1)
| ~ strong(p1)
| ~ aee(p1,X122)
| bearer(skolem0003(p1,X122,museen,read,museum_api,e1),museen) ),
inference(resolution,[status(thm)],[c64,c7]) ).
cnf(c67,plain,
( ~ perm(p1)
| ~ strong(p1)
| bearer(skolem0003(p1,bibliothek,museen,read,museum_api,e1),museen) ),
inference(resolution,[status(thm)],[c66,c8]) ).
cnf(c68,plain,
( ~ perm(p1)
| bearer(skolem0003(p1,bibliothek,museen,read,museum_api,e1),museen) ),
inference(resolution,[status(thm)],[c67,c9]) ).
cnf(c69,plain,
bearer(skolem0003(p1,bibliothek,museen,read,museum_api,e1),museen),
inference(resolution,[status(thm)],[c68,c10]) ).
cnf(c21,plain,
( ~ perm(X35)
| ~ strong(X35)
| ~ aee(X35,X37)
| ~ aer(X35,X36)
| ~ act(X35,X34)
| ~ tgt(X35,X38)
| ~ activates(X33,X35)
| founds_imm(X33,skolem0001(X35,X37,X36,X34,X38,X33),X35) ),
inference(split_conjunct,[status(thm)],[c20]) ).
cnf(c33,plain,
( ~ perm(p1)
| ~ strong(p1)
| ~ aee(p1,X100)
| ~ aer(p1,X99)
| ~ act(p1,X102)
| ~ tgt(p1,X101)
| founds_imm(e1,skolem0001(p1,X100,X99,X102,X101,e1),p1) ),
inference(resolution,[status(thm)],[c21,c4]) ).
cnf(c55,plain,
( ~ perm(p1)
| ~ strong(p1)
| ~ aee(p1,X105)
| ~ aer(p1,X104)
| ~ act(p1,X103)
| founds_imm(e1,skolem0001(p1,X105,X104,X103,museum_api,e1),p1) ),
inference(resolution,[status(thm)],[c33,c5]) ).
cnf(c58,plain,
( ~ perm(p1)
| ~ strong(p1)
| ~ aee(p1,X106)
| ~ aer(p1,X107)
| founds_imm(e1,skolem0001(p1,X106,X107,read,museum_api,e1),p1) ),
inference(resolution,[status(thm)],[c55,c6]) ).
cnf(c59,plain,
( ~ perm(p1)
| ~ strong(p1)
| ~ aee(p1,X112)
| founds_imm(e1,skolem0001(p1,X112,museen,read,museum_api,e1),p1) ),
inference(resolution,[status(thm)],[c58,c7]) ).
cnf(c61,plain,
( ~ perm(p1)
| ~ strong(p1)
| founds_imm(e1,skolem0001(p1,bibliothek,museen,read,museum_api,e1),p1) ),
inference(resolution,[status(thm)],[c59,c8]) ).
cnf(c62,plain,
( ~ perm(p1)
| founds_imm(e1,skolem0001(p1,bibliothek,museen,read,museum_api,e1),p1) ),
inference(resolution,[status(thm)],[c61,c9]) ).
cnf(c63,plain,
founds_imm(e1,skolem0001(p1,bibliothek,museen,read,museum_api,e1),p1),
inference(resolution,[status(thm)],[c62,c10]) ).
fof(conjecture,conjecture,
? [RhoI,Db] :
( founds_imm(e1,RhoI,p1)
& disability(Db)
& bearer(Db,museen)
& cnt(Db,read,museum_api)
& part_of(Db,RhoI) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture) ).
fof(c0,negated_conjecture,
~ ? [RhoI,Db] :
( founds_imm(e1,RhoI,p1)
& disability(Db)
& bearer(Db,museen)
& cnt(Db,read,museum_api)
& part_of(Db,RhoI) ),
inference(assume_negation,[status(cth)],[conjecture]) ).
fof(c1,negated_conjecture,
! [RhoI,Db] :
( ~ founds_imm(e1,RhoI,p1)
| ~ disability(Db)
| ~ bearer(Db,museen)
| ~ cnt(Db,read,museum_api)
| ~ part_of(Db,RhoI) ),
inference(fof_nnf,[status(thm)],[c0]) ).
fof(c2,negated_conjecture,
! [X2,X3] :
( ~ founds_imm(e1,X2,p1)
| ~ disability(X3)
| ~ bearer(X3,museen)
| ~ cnt(X3,read,museum_api)
| ~ part_of(X3,X2) ),
inference(variable_rename,[status(thm)],[c1]) ).
cnf(c3,negated_conjecture,
( ~ founds_imm(e1,X13,p1)
| ~ disability(X14)
| ~ bearer(X14,museen)
| ~ cnt(X14,read,museum_api)
| ~ part_of(X14,X13) ),
inference(split_conjunct,[status(thm)],[c2]) ).
cnf(c28,plain,
( ~ perm(X53)
| ~ strong(X53)
| ~ aee(X53,X55)
| ~ aer(X53,X54)
| ~ act(X53,X52)
| ~ tgt(X53,X56)
| ~ activates(X51,X53)
| cnt(skolem0003(X53,X55,X54,X52,X56,X51),X52,X56) ),
inference(split_conjunct,[status(thm)],[c20]) ).
cnf(c36,plain,
( ~ perm(p1)
| ~ strong(p1)
| ~ aee(p1,X125)
| ~ aer(p1,X126)
| ~ act(p1,X123)
| ~ tgt(p1,X124)
| cnt(skolem0003(p1,X125,X126,X123,X124,e1),X123,X124) ),
inference(resolution,[status(thm)],[c28,c4]) ).
cnf(c70,plain,
( ~ perm(p1)
| ~ strong(p1)
| ~ aee(p1,X137)
| ~ aer(p1,X138)
| ~ act(p1,X139)
| cnt(skolem0003(p1,X137,X138,X139,museum_api,e1),X139,museum_api) ),
inference(resolution,[status(thm)],[c36,c5]) ).
cnf(c78,plain,
( ~ perm(p1)
| ~ strong(p1)
| ~ aee(p1,X141)
| ~ aer(p1,X140)
| cnt(skolem0003(p1,X141,X140,read,museum_api,e1),read,museum_api) ),
inference(resolution,[status(thm)],[c70,c6]) ).
cnf(c79,plain,
( ~ perm(p1)
| ~ strong(p1)
| ~ aee(p1,X142)
| cnt(skolem0003(p1,X142,museen,read,museum_api,e1),read,museum_api) ),
inference(resolution,[status(thm)],[c78,c7]) ).
cnf(c80,plain,
( ~ perm(p1)
| ~ strong(p1)
| cnt(skolem0003(p1,bibliothek,museen,read,museum_api,e1),read,museum_api) ),
inference(resolution,[status(thm)],[c79,c8]) ).
cnf(c81,plain,
( ~ perm(p1)
| cnt(skolem0003(p1,bibliothek,museen,read,museum_api,e1),read,museum_api) ),
inference(resolution,[status(thm)],[c80,c9]) ).
cnf(c83,plain,
cnt(skolem0003(p1,bibliothek,museen,read,museum_api,e1),read,museum_api),
inference(resolution,[status(thm)],[c81,c10]) ).
cnf(c84,plain,
( ~ founds_imm(e1,X159,p1)
| ~ disability(skolem0003(p1,bibliothek,museen,read,museum_api,e1))
| ~ bearer(skolem0003(p1,bibliothek,museen,read,museum_api,e1),museen)
| ~ part_of(skolem0003(p1,bibliothek,museen,read,museum_api,e1),X159) ),
inference(resolution,[status(thm)],[c83,c3]) ).
cnf(c29,plain,
( ~ perm(X75)
| ~ strong(X75)
| ~ aee(X75,X77)
| ~ aer(X75,X76)
| ~ act(X75,X74)
| ~ tgt(X75,X78)
| ~ activates(X73,X75)
| part_of(skolem0003(X75,X77,X76,X74,X78,X73),skolem0001(X75,X77,X76,X74,X78,X73)) ),
inference(split_conjunct,[status(thm)],[c20]) ).
cnf(c44,plain,
( ~ perm(p1)
| ~ strong(p1)
| ~ aee(p1,X145)
| ~ aer(p1,X143)
| ~ act(p1,X146)
| ~ tgt(p1,X144)
| part_of(skolem0003(p1,X145,X143,X146,X144,e1),skolem0001(p1,X145,X143,X146,X144,e1)) ),
inference(resolution,[status(thm)],[c29,c4]) ).
cnf(c82,plain,
( ~ perm(p1)
| ~ strong(p1)
| ~ aee(p1,X154)
| ~ aer(p1,X156)
| ~ act(p1,X155)
| part_of(skolem0003(p1,X154,X156,X155,museum_api,e1),skolem0001(p1,X154,X156,X155,museum_api,e1)) ),
inference(resolution,[status(thm)],[c44,c5]) ).
cnf(c91,plain,
( ~ perm(p1)
| ~ strong(p1)
| ~ aee(p1,X158)
| ~ aer(p1,X157)
| part_of(skolem0003(p1,X158,X157,read,museum_api,e1),skolem0001(p1,X158,X157,read,museum_api,e1)) ),
inference(resolution,[status(thm)],[c82,c6]) ).
cnf(c92,plain,
( ~ perm(p1)
| ~ strong(p1)
| ~ aee(p1,X160)
| part_of(skolem0003(p1,X160,museen,read,museum_api,e1),skolem0001(p1,X160,museen,read,museum_api,e1)) ),
inference(resolution,[status(thm)],[c91,c7]) ).
cnf(c93,plain,
( ~ perm(p1)
| ~ strong(p1)
| part_of(skolem0003(p1,bibliothek,museen,read,museum_api,e1),skolem0001(p1,bibliothek,museen,read,museum_api,e1)) ),
inference(resolution,[status(thm)],[c92,c8]) ).
cnf(c94,plain,
( ~ perm(p1)
| part_of(skolem0003(p1,bibliothek,museen,read,museum_api,e1),skolem0001(p1,bibliothek,museen,read,museum_api,e1)) ),
inference(resolution,[status(thm)],[c93,c9]) ).
cnf(c95,plain,
part_of(skolem0003(p1,bibliothek,museen,read,museum_api,e1),skolem0001(p1,bibliothek,museen,read,museum_api,e1)),
inference(resolution,[status(thm)],[c94,c10]) ).
cnf(c96,plain,
( ~ founds_imm(e1,skolem0001(p1,bibliothek,museen,read,museum_api,e1),p1)
| ~ disability(skolem0003(p1,bibliothek,museen,read,museum_api,e1))
| ~ bearer(skolem0003(p1,bibliothek,museen,read,museum_api,e1),museen) ),
inference(resolution,[status(thm)],[c95,c84]) ).
cnf(c98,plain,
( ~ disability(skolem0003(p1,bibliothek,museen,read,museum_api,e1))
| ~ bearer(skolem0003(p1,bibliothek,museen,read,museum_api,e1),museen) ),
inference(resolution,[status(thm)],[c96,c63]) ).
cnf(c99,plain,
~ disability(skolem0003(p1,bibliothek,museen,read,museum_api,e1)),
inference(resolution,[status(thm)],[c98,c69]) ).
cnf(c100,plain,
$false,
inference(resolution,[status(thm)],[c99,c51]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT117+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.35 % Computer : n014.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 7 14:09:41 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.13/0.41 (re.compile("\."), Token.FullStop),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.13/0.41 (re.compile("\("), Token.OpenPar),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.13/0.41 (re.compile("\)"), Token.ClosePar),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.13/0.41 (re.compile("\["), Token.OpenSquare),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.13/0.41 (re.compile("\]"), Token.CloseSquare),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.41 (re.compile("~\|"), Token.Nor),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.41 (re.compile("\|"), Token.Or),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.13/0.41 (re.compile("\?"), Token.Existential),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.13/0.41 (re.compile("\s+"), Token.WhiteSpace),
% 0.13/0.41 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.13/0.41 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.22/0.48 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.48 """
% 0.22/0.49 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.22/0.49 """
% 0.32/0.58 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.32/0.58 """
% 0.39/0.66 % Version: 1.5
% 0.39/0.66 % SZS status Theorem
% 0.39/0.66 % SZS output start CNFRefutation
% See solution above
% 0.39/0.67
% 0.39/0.67 % Initial clauses : 23
% 0.39/0.67 % Processed clauses : 93
% 0.39/0.67 % Factors computed : 0
% 0.39/0.67 % Resolvents computed: 71
% 0.39/0.67 % Tautologies deleted: 0
% 0.39/0.67 % Forward subsumed : 0
% 0.39/0.67 % Backward subsumed : 23
% 0.39/0.67 % -------- CPU Time ---------
% 0.39/0.67 % User time : 0.293 s
% 0.39/0.67 % System time : 0.019 s
% 0.39/0.67 % Total time : 0.312 s
%------------------------------------------------------------------------------