%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR039+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Sun Sep 27 07:03:52 AM UTC 2026
% Result : Theorem 20.75s 4.56s
% Output : CNFRefutation 20.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 32
% Syntax : Number of formulae : 119 ( 83 unt; 0 def)
% Number of atoms : 161 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 77 ( 35 ~; 33 |; 3 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 33 ( 33 usr; 30 con; 0-2 aty)
% Number of variables : 48 ( 0 sgn 11 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(just7,axiom,
genls('c$utptpcol$u2$u2','c$utptpcol$u1$u1') ).
fof(just9,axiom,
genls('c$utptpcol$u3$u16386','c$utptpcol$u2$u2') ).
fof(just11,axiom,
genls('c$utptpcol$u4$u16387','c$utptpcol$u3$u16386') ).
fof(just13,axiom,
genls('c$utptpcol$u5$u16388','c$utptpcol$u4$u16387') ).
fof(just15,axiom,
genls('c$utptpcol$u6$u18436','c$utptpcol$u5$u16388') ).
fof(just17,axiom,
genls('c$utptpcol$u7$u18437','c$utptpcol$u6$u18436') ).
fof(just19,axiom,
genls('c$utptpcol$u8$u18438','c$utptpcol$u7$u18437') ).
fof(just21,axiom,
genls('c$utptpcol$u9$u18439','c$utptpcol$u8$u18438') ).
fof(just23,axiom,
genls('c$utptpcol$u10$u18567','c$utptpcol$u9$u18439') ).
fof(just25,axiom,
genls('c$utptpcol$u11$u18631','c$utptpcol$u10$u18567') ).
fof(just27,axiom,
genls('c$utptpcol$u12$u18663','c$utptpcol$u11$u18631') ).
fof(just29,axiom,
genls('c$utptpcol$u13$u18664','c$utptpcol$u12$u18663') ).
fof(just31,axiom,
genls('c$utptpcol$u2$u65537','c$utptpcol$u1$u65536') ).
fof(just33,axiom,
genls('c$utptpcol$u3$u81921','c$utptpcol$u2$u65537') ).
fof(just35,axiom,
genls('c$utptpcol$u4$u90113','c$utptpcol$u3$u81921') ).
fof(just37,axiom,
genls('c$utptpcol$u5$u90114','c$utptpcol$u4$u90113') ).
fof(just39,axiom,
genls('c$utptpcol$u6$u92162','c$utptpcol$u5$u90114') ).
fof(just41,axiom,
genls('c$utptpcol$u7$u93186','c$utptpcol$u6$u92162') ).
fof(just43,axiom,
genls('c$utptpcol$u8$u93698','c$utptpcol$u7$u93186') ).
fof(just45,axiom,
genls('c$utptpcol$u9$u93699','c$utptpcol$u8$u93698') ).
fof(just47,axiom,
genls('c$utptpcol$u10$u93700','c$utptpcol$u9$u93699') ).
fof(just49,axiom,
genls('c$utptpcol$u11$u93764','c$utptpcol$u10$u93700') ).
fof(just51,axiom,
genls('c$utptpcol$u12$u93765','c$utptpcol$u11$u93764') ).
fof(just53,axiom,
genls('c$utptpcol$u13$u93766','c$utptpcol$u12$u93765') ).
fof(just55,axiom,
genls('c$utptpcol$u14$u93774','c$utptpcol$u13$u93766') ).
fof(just57,axiom,
genls('c$utptpcol$u15$u93775','c$utptpcol$u14$u93774') ).
fof(just59,axiom,
disjointwith('c$utptpcol$u1$u1','c$utptpcol$u1$u65536') ).
fof(just76,axiom,
! [X0,X1] :
( disjointwith(X0,X1)
=> disjointwith(X1,X0) ) ).
fof(just77,axiom,
! [X0,X1,X2] :
( ( genls(X2,X1)
& disjointwith(X0,X1) )
=> disjointwith(X0,X2) ) ).
fof(just78,axiom,
! [X0,X1,X2] :
( ( genls(X2,X0)
& disjointwith(X0,X1) )
=> disjointwith(X2,X1) ) ).
fof(just139,axiom,
! [X0,X1,X2] :
( ( genls(X1,X2)
& genls(X0,X1) )
=> genls(X0,X2) ) ).
fof(query39,conjecture,
( mtvisible('f$ucontentmtofcdafromeventfn'('f$uurlreferentfn'('f$uurlfn'('s$uhttp$uwwwpoweripodsearchinfobrown$uipodhtml')),'c$utranslation$u7'))
=> disjointwith('c$utptpcol$u15$u93775','c$utptpcol$u13$u18664') ) ).
fof(negated_conjecture,negated_conjecture,
~ ( mtvisible('f$ucontentmtofcdafromeventfn'('f$uurlreferentfn'('f$uurlfn'('s$uhttp$uwwwpoweripodsearchinfobrown$uipodhtml')),'c$utranslation$u7'))
=> disjointwith('c$utptpcol$u15$u93775','c$utptpcol$u13$u18664') ),
inference(negate_conjecture,[status(cth)],[query39]) ).
cnf(c6,plain,
genls('c$utptpcol$u2$u2','c$utptpcol$u1$u1'),
inference(clausification,[status(esa)],[just7]) ).
cnf(c8,plain,
genls('c$utptpcol$u3$u16386','c$utptpcol$u2$u2'),
inference(clausification,[status(esa)],[just9]) ).
cnf(c10,plain,
genls('c$utptpcol$u4$u16387','c$utptpcol$u3$u16386'),
inference(clausification,[status(esa)],[just11]) ).
cnf(c12,plain,
genls('c$utptpcol$u5$u16388','c$utptpcol$u4$u16387'),
inference(clausification,[status(esa)],[just13]) ).
cnf(c14,plain,
genls('c$utptpcol$u6$u18436','c$utptpcol$u5$u16388'),
inference(clausification,[status(esa)],[just15]) ).
cnf(c16,plain,
genls('c$utptpcol$u7$u18437','c$utptpcol$u6$u18436'),
inference(clausification,[status(esa)],[just17]) ).
cnf(c18,plain,
genls('c$utptpcol$u8$u18438','c$utptpcol$u7$u18437'),
inference(clausification,[status(esa)],[just19]) ).
cnf(c20,plain,
genls('c$utptpcol$u9$u18439','c$utptpcol$u8$u18438'),
inference(clausification,[status(esa)],[just21]) ).
cnf(c22,plain,
genls('c$utptpcol$u10$u18567','c$utptpcol$u9$u18439'),
inference(clausification,[status(esa)],[just23]) ).
cnf(c24,plain,
genls('c$utptpcol$u11$u18631','c$utptpcol$u10$u18567'),
inference(clausification,[status(esa)],[just25]) ).
cnf(c26,plain,
genls('c$utptpcol$u12$u18663','c$utptpcol$u11$u18631'),
inference(clausification,[status(esa)],[just27]) ).
cnf(c28,plain,
genls('c$utptpcol$u13$u18664','c$utptpcol$u12$u18663'),
inference(clausification,[status(esa)],[just29]) ).
cnf(c30,plain,
genls('c$utptpcol$u2$u65537','c$utptpcol$u1$u65536'),
inference(clausification,[status(esa)],[just31]) ).
cnf(c32,plain,
genls('c$utptpcol$u3$u81921','c$utptpcol$u2$u65537'),
inference(clausification,[status(esa)],[just33]) ).
cnf(c34,plain,
genls('c$utptpcol$u4$u90113','c$utptpcol$u3$u81921'),
inference(clausification,[status(esa)],[just35]) ).
cnf(c36,plain,
genls('c$utptpcol$u5$u90114','c$utptpcol$u4$u90113'),
inference(clausification,[status(esa)],[just37]) ).
cnf(c38,plain,
genls('c$utptpcol$u6$u92162','c$utptpcol$u5$u90114'),
inference(clausification,[status(esa)],[just39]) ).
cnf(c40,plain,
genls('c$utptpcol$u7$u93186','c$utptpcol$u6$u92162'),
inference(clausification,[status(esa)],[just41]) ).
cnf(c42,plain,
genls('c$utptpcol$u8$u93698','c$utptpcol$u7$u93186'),
inference(clausification,[status(esa)],[just43]) ).
cnf(c44,plain,
genls('c$utptpcol$u9$u93699','c$utptpcol$u8$u93698'),
inference(clausification,[status(esa)],[just45]) ).
cnf(c46,plain,
genls('c$utptpcol$u10$u93700','c$utptpcol$u9$u93699'),
inference(clausification,[status(esa)],[just47]) ).
cnf(c48,plain,
genls('c$utptpcol$u11$u93764','c$utptpcol$u10$u93700'),
inference(clausification,[status(esa)],[just49]) ).
cnf(c50,plain,
genls('c$utptpcol$u12$u93765','c$utptpcol$u11$u93764'),
inference(clausification,[status(esa)],[just51]) ).
cnf(c52,plain,
genls('c$utptpcol$u13$u93766','c$utptpcol$u12$u93765'),
inference(clausification,[status(esa)],[just53]) ).
cnf(c54,plain,
genls('c$utptpcol$u14$u93774','c$utptpcol$u13$u93766'),
inference(clausification,[status(esa)],[just55]) ).
cnf(c56,plain,
genls('c$utptpcol$u15$u93775','c$utptpcol$u14$u93774'),
inference(clausification,[status(esa)],[just57]) ).
cnf(c58,plain,
disjointwith('c$utptpcol$u1$u1','c$utptpcol$u1$u65536'),
inference(clausification,[status(esa)],[just59]) ).
cnf(c75,plain,
( disjointwith(X1,X0)
| ~ disjointwith(X0,X1) ),
inference(clausification,[status(esa)],[just76]) ).
cnf(c76,plain,
( disjointwith(X0,X2)
| ~ genls(X2,X1)
| ~ disjointwith(X0,X1) ),
inference(clausification,[status(esa)],[just77]) ).
cnf(c77,plain,
( disjointwith(X2,X1)
| ~ genls(X2,X0)
| ~ disjointwith(X0,X1) ),
inference(clausification,[status(esa)],[just78]) ).
cnf(c138,plain,
( genls(X0,X2)
| ~ genls(X1,X2)
| ~ genls(X0,X1) ),
inference(clausification,[status(esa)],[just139]) ).
cnf(c171,plain,
~ disjointwith('c$utptpcol$u15$u93775','c$utptpcol$u13$u18664'),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ genls(X0,'c$utptpcol$u2$u65537')
| genls(X0,'c$utptpcol$u1$u65536') ),
inference(resolution,[status(thm)],[c138,c30]) ).
cnf(d1,plain,
( ~ genls(X0,'c$utptpcol$u3$u81921')
| genls(X0,'c$utptpcol$u2$u65537') ),
inference(resolution,[status(thm)],[c138,c32]) ).
cnf(d2,plain,
( ~ genls(X0,'c$utptpcol$u4$u90113')
| genls(X0,'c$utptpcol$u3$u81921') ),
inference(resolution,[status(thm)],[c138,c34]) ).
cnf(d3,plain,
( ~ genls(X0,'c$utptpcol$u5$u90114')
| genls(X0,'c$utptpcol$u4$u90113') ),
inference(resolution,[status(thm)],[c138,c36]) ).
cnf(d4,plain,
( ~ genls(X0,'c$utptpcol$u6$u92162')
| genls(X0,'c$utptpcol$u5$u90114') ),
inference(resolution,[status(thm)],[c138,c38]) ).
cnf(d5,plain,
( ~ genls(X0,'c$utptpcol$u7$u93186')
| genls(X0,'c$utptpcol$u6$u92162') ),
inference(resolution,[status(thm)],[c138,c40]) ).
cnf(d6,plain,
( ~ genls(X0,'c$utptpcol$u8$u93698')
| genls(X0,'c$utptpcol$u7$u93186') ),
inference(resolution,[status(thm)],[c138,c42]) ).
cnf(d7,plain,
( ~ genls(X0,'c$utptpcol$u9$u93699')
| genls(X0,'c$utptpcol$u8$u93698') ),
inference(resolution,[status(thm)],[c138,c44]) ).
cnf(d8,plain,
( ~ genls(X0,'c$utptpcol$u10$u93700')
| genls(X0,'c$utptpcol$u9$u93699') ),
inference(resolution,[status(thm)],[c138,c46]) ).
cnf(d9,plain,
( ~ genls(X0,'c$utptpcol$u11$u93764')
| genls(X0,'c$utptpcol$u10$u93700') ),
inference(resolution,[status(thm)],[c138,c48]) ).
cnf(d10,plain,
( ~ genls(X0,'c$utptpcol$u12$u93765')
| genls(X0,'c$utptpcol$u11$u93764') ),
inference(resolution,[status(thm)],[c138,c50]) ).
cnf(d11,plain,
( ~ genls(X0,'c$utptpcol$u13$u93766')
| genls(X0,'c$utptpcol$u12$u93765') ),
inference(resolution,[status(thm)],[c138,c52]) ).
cnf(d12,plain,
( ~ genls(X0,'c$utptpcol$u14$u93774')
| genls(X0,'c$utptpcol$u13$u93766') ),
inference(resolution,[status(thm)],[c138,c54]) ).
cnf(d13,plain,
genls('c$utptpcol$u15$u93775','c$utptpcol$u13$u93766'),
inference(resolution,[status(thm)],[d12,c56]) ).
cnf(d14,plain,
genls('c$utptpcol$u15$u93775','c$utptpcol$u12$u93765'),
inference(resolution,[status(thm)],[d13,d11]) ).
cnf(d15,plain,
genls('c$utptpcol$u15$u93775','c$utptpcol$u11$u93764'),
inference(resolution,[status(thm)],[d14,d10]) ).
cnf(d16,plain,
genls('c$utptpcol$u15$u93775','c$utptpcol$u10$u93700'),
inference(resolution,[status(thm)],[d15,d9]) ).
cnf(d17,plain,
genls('c$utptpcol$u15$u93775','c$utptpcol$u9$u93699'),
inference(resolution,[status(thm)],[d16,d8]) ).
cnf(d18,plain,
genls('c$utptpcol$u15$u93775','c$utptpcol$u8$u93698'),
inference(resolution,[status(thm)],[d17,d7]) ).
cnf(d19,plain,
genls('c$utptpcol$u15$u93775','c$utptpcol$u7$u93186'),
inference(resolution,[status(thm)],[d18,d6]) ).
cnf(d20,plain,
genls('c$utptpcol$u15$u93775','c$utptpcol$u6$u92162'),
inference(resolution,[status(thm)],[d19,d5]) ).
cnf(d21,plain,
genls('c$utptpcol$u15$u93775','c$utptpcol$u5$u90114'),
inference(resolution,[status(thm)],[d20,d4]) ).
cnf(d22,plain,
genls('c$utptpcol$u15$u93775','c$utptpcol$u4$u90113'),
inference(resolution,[status(thm)],[d21,d3]) ).
cnf(d23,plain,
genls('c$utptpcol$u15$u93775','c$utptpcol$u3$u81921'),
inference(resolution,[status(thm)],[d22,d2]) ).
cnf(d24,plain,
genls('c$utptpcol$u15$u93775','c$utptpcol$u2$u65537'),
inference(resolution,[status(thm)],[d23,d1]) ).
cnf(d25,plain,
genls('c$utptpcol$u15$u93775','c$utptpcol$u1$u65536'),
inference(resolution,[status(thm)],[d24,d0]) ).
cnf(d26,plain,
disjointwith('c$utptpcol$u1$u65536','c$utptpcol$u1$u1'),
inference(resolution,[status(thm)],[c75,c58]) ).
cnf(d27,plain,
( disjointwith('c$utptpcol$u1$u65536',X0)
| ~ genls(X0,'c$utptpcol$u1$u1') ),
inference(resolution,[status(thm)],[d26,c76]) ).
cnf(d28,plain,
( ~ genls(X0,'c$utptpcol$u2$u2')
| genls(X0,'c$utptpcol$u1$u1') ),
inference(resolution,[status(thm)],[c138,c6]) ).
cnf(d29,plain,
( ~ genls(X0,'c$utptpcol$u3$u16386')
| genls(X0,'c$utptpcol$u2$u2') ),
inference(resolution,[status(thm)],[c138,c8]) ).
cnf(d30,plain,
( ~ genls(X0,'c$utptpcol$u4$u16387')
| genls(X0,'c$utptpcol$u3$u16386') ),
inference(resolution,[status(thm)],[c138,c10]) ).
cnf(d31,plain,
( ~ genls(X0,'c$utptpcol$u5$u16388')
| genls(X0,'c$utptpcol$u4$u16387') ),
inference(resolution,[status(thm)],[c138,c12]) ).
cnf(d32,plain,
( ~ genls(X0,'c$utptpcol$u6$u18436')
| genls(X0,'c$utptpcol$u5$u16388') ),
inference(resolution,[status(thm)],[c138,c14]) ).
cnf(d33,plain,
( ~ genls(X0,'c$utptpcol$u7$u18437')
| genls(X0,'c$utptpcol$u6$u18436') ),
inference(resolution,[status(thm)],[c138,c16]) ).
cnf(d34,plain,
( ~ genls(X0,'c$utptpcol$u8$u18438')
| genls(X0,'c$utptpcol$u7$u18437') ),
inference(resolution,[status(thm)],[c138,c18]) ).
cnf(d35,plain,
( ~ genls(X0,'c$utptpcol$u9$u18439')
| genls(X0,'c$utptpcol$u8$u18438') ),
inference(resolution,[status(thm)],[c138,c20]) ).
cnf(d36,plain,
( ~ genls(X0,'c$utptpcol$u10$u18567')
| genls(X0,'c$utptpcol$u9$u18439') ),
inference(resolution,[status(thm)],[c138,c22]) ).
cnf(d37,plain,
( ~ genls(X0,'c$utptpcol$u11$u18631')
| genls(X0,'c$utptpcol$u10$u18567') ),
inference(resolution,[status(thm)],[c138,c24]) ).
cnf(d38,plain,
( ~ genls(X0,'c$utptpcol$u12$u18663')
| genls(X0,'c$utptpcol$u11$u18631') ),
inference(resolution,[status(thm)],[c138,c26]) ).
cnf(d39,plain,
genls('c$utptpcol$u13$u18664','c$utptpcol$u11$u18631'),
inference(resolution,[status(thm)],[d38,c28]) ).
cnf(d40,plain,
genls('c$utptpcol$u13$u18664','c$utptpcol$u10$u18567'),
inference(resolution,[status(thm)],[d39,d37]) ).
cnf(d41,plain,
genls('c$utptpcol$u13$u18664','c$utptpcol$u9$u18439'),
inference(resolution,[status(thm)],[d40,d36]) ).
cnf(d42,plain,
genls('c$utptpcol$u13$u18664','c$utptpcol$u8$u18438'),
inference(resolution,[status(thm)],[d41,d35]) ).
cnf(d43,plain,
genls('c$utptpcol$u13$u18664','c$utptpcol$u7$u18437'),
inference(resolution,[status(thm)],[d42,d34]) ).
cnf(d44,plain,
genls('c$utptpcol$u13$u18664','c$utptpcol$u6$u18436'),
inference(resolution,[status(thm)],[d43,d33]) ).
cnf(d45,plain,
genls('c$utptpcol$u13$u18664','c$utptpcol$u5$u16388'),
inference(resolution,[status(thm)],[d44,d32]) ).
cnf(d46,plain,
genls('c$utptpcol$u13$u18664','c$utptpcol$u4$u16387'),
inference(resolution,[status(thm)],[d45,d31]) ).
cnf(d47,plain,
genls('c$utptpcol$u13$u18664','c$utptpcol$u3$u16386'),
inference(resolution,[status(thm)],[d46,d30]) ).
cnf(d48,plain,
genls('c$utptpcol$u13$u18664','c$utptpcol$u2$u2'),
inference(resolution,[status(thm)],[d47,d29]) ).
cnf(d49,plain,
genls('c$utptpcol$u13$u18664','c$utptpcol$u1$u1'),
inference(resolution,[status(thm)],[d48,d28]) ).
cnf(d50,plain,
disjointwith('c$utptpcol$u1$u65536','c$utptpcol$u13$u18664'),
inference(resolution,[status(thm)],[d49,d27]) ).
cnf(d51,plain,
( disjointwith(X0,'c$utptpcol$u13$u18664')
| ~ genls(X0,'c$utptpcol$u1$u65536') ),
inference(resolution,[status(thm)],[d50,c77]) ).
cnf(d52,plain,
disjointwith('c$utptpcol$u15$u93775','c$utptpcol$u13$u18664'),
inference(resolution,[status(thm)],[d51,d25]) ).
cnf(d53,plain,
$false,
inference(resolution,[status(thm)],[c171,d52]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR039+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n014.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 00:09:01 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.75/4.56 % SZS status Theorem for theBenchmark.p
% 20.75/4.56 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------