%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR036+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 : n026.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:50 AM UTC 2026
% Result : Theorem 42.55s 5.83s
% Output : CNFRefutation 42.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 34
% Syntax : Number of formulae : 128 ( 91 unt; 0 def)
% Number of atoms : 171 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 80 ( 37 ~; 35 |; 3 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 32 con; 0-0 aty)
% Number of variables : 47 ( 0 sgn 9 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(just6,axiom,
genls('c$utptpcol$u2$u2','c$utptpcol$u1$u1') ).
fof(just8,axiom,
genls('c$utptpcol$u3$u16386','c$utptpcol$u2$u2') ).
fof(just10,axiom,
genls('c$utptpcol$u4$u16387','c$utptpcol$u3$u16386') ).
fof(just12,axiom,
genls('c$utptpcol$u5$u20483','c$utptpcol$u4$u16387') ).
fof(just14,axiom,
genls('c$utptpcol$u6$u20484','c$utptpcol$u5$u20483') ).
fof(just16,axiom,
genls('c$utptpcol$u7$u21508','c$utptpcol$u6$u20484') ).
fof(just18,axiom,
genls('c$utptpcol$u8$u22020','c$utptpcol$u7$u21508') ).
fof(just20,axiom,
genls('c$utptpcol$u9$u22021','c$utptpcol$u8$u22020') ).
fof(just22,axiom,
genls('c$utptpcol$u10$u22022','c$utptpcol$u9$u22021') ).
fof(just24,axiom,
genls('c$utptpcol$u11$u22023','c$utptpcol$u10$u22022') ).
fof(just26,axiom,
genls('c$utptpcol$u12$u22055','c$utptpcol$u11$u22023') ).
fof(just28,axiom,
genls('c$utptpcol$u13$u22071','c$utptpcol$u12$u22055') ).
fof(just30,axiom,
genls('c$utptpcol$u14$u22072','c$utptpcol$u13$u22071') ).
fof(just32,axiom,
genls('c$utptpcol$u15$u22076','c$utptpcol$u14$u22072') ).
fof(just34,axiom,
genls('c$utptpcol$u2$u65537','c$utptpcol$u1$u65536') ).
fof(just36,axiom,
genls('c$utptpcol$u3$u65538','c$utptpcol$u2$u65537') ).
fof(just38,axiom,
genls('c$utptpcol$u4$u65539','c$utptpcol$u3$u65538') ).
fof(just40,axiom,
genls('c$utptpcol$u5$u69635','c$utptpcol$u4$u65539') ).
fof(just42,axiom,
genls('c$utptpcol$u6$u71683','c$utptpcol$u5$u69635') ).
fof(just44,axiom,
genls('c$utptpcol$u7$u72707','c$utptpcol$u6$u71683') ).
fof(just46,axiom,
genls('c$utptpcol$u8$u72708','c$utptpcol$u7$u72707') ).
fof(just48,axiom,
genls('c$utptpcol$u9$u72709','c$utptpcol$u8$u72708') ).
fof(just50,axiom,
genls('c$utptpcol$u10$u72710','c$utptpcol$u9$u72709') ).
fof(just52,axiom,
genls('c$utptpcol$u11$u72774','c$utptpcol$u10$u72710') ).
fof(just54,axiom,
genls('c$utptpcol$u12$u72775','c$utptpcol$u11$u72774') ).
fof(just56,axiom,
genls('c$utptpcol$u13$u72791','c$utptpcol$u12$u72775') ).
fof(just58,axiom,
genls('c$utptpcol$u14$u72792','c$utptpcol$u13$u72791') ).
fof(just60,axiom,
genls('c$utptpcol$u15$u72793','c$utptpcol$u14$u72792') ).
fof(just62,axiom,
genls('c$utptpcol$u16$u72795','c$utptpcol$u15$u72793') ).
fof(just64,axiom,
disjointwith('c$utptpcol$u1$u1','c$utptpcol$u1$u65536') ).
fof(just84,axiom,
! [X0,X1,X2] :
( ( genls(X2,X1)
& disjointwith(X0,X1) )
=> disjointwith(X0,X2) ) ).
fof(just85,axiom,
! [X0,X1,X2] :
( ( genls(X2,X0)
& disjointwith(X0,X1) )
=> disjointwith(X2,X1) ) ).
fof(just152,axiom,
! [X0,X1,X2] :
( ( genls(X1,X2)
& genls(X0,X1) )
=> genls(X0,X2) ) ).
fof(query36,conjecture,
( mtvisible('c$utptp$umember974$umt')
=> disjointwith('c$utptpcol$u15$u22076','c$utptpcol$u16$u72795') ) ).
fof(negated_conjecture,negated_conjecture,
~ ( mtvisible('c$utptp$umember974$umt')
=> disjointwith('c$utptpcol$u15$u22076','c$utptpcol$u16$u72795') ),
inference(negate_conjecture,[status(cth)],[query36]) ).
cnf(c5,plain,
genls('c$utptpcol$u2$u2','c$utptpcol$u1$u1'),
inference(clausification,[status(esa)],[just6]) ).
cnf(c7,plain,
genls('c$utptpcol$u3$u16386','c$utptpcol$u2$u2'),
inference(clausification,[status(esa)],[just8]) ).
cnf(c9,plain,
genls('c$utptpcol$u4$u16387','c$utptpcol$u3$u16386'),
inference(clausification,[status(esa)],[just10]) ).
cnf(c11,plain,
genls('c$utptpcol$u5$u20483','c$utptpcol$u4$u16387'),
inference(clausification,[status(esa)],[just12]) ).
cnf(c13,plain,
genls('c$utptpcol$u6$u20484','c$utptpcol$u5$u20483'),
inference(clausification,[status(esa)],[just14]) ).
cnf(c15,plain,
genls('c$utptpcol$u7$u21508','c$utptpcol$u6$u20484'),
inference(clausification,[status(esa)],[just16]) ).
cnf(c17,plain,
genls('c$utptpcol$u8$u22020','c$utptpcol$u7$u21508'),
inference(clausification,[status(esa)],[just18]) ).
cnf(c19,plain,
genls('c$utptpcol$u9$u22021','c$utptpcol$u8$u22020'),
inference(clausification,[status(esa)],[just20]) ).
cnf(c21,plain,
genls('c$utptpcol$u10$u22022','c$utptpcol$u9$u22021'),
inference(clausification,[status(esa)],[just22]) ).
cnf(c23,plain,
genls('c$utptpcol$u11$u22023','c$utptpcol$u10$u22022'),
inference(clausification,[status(esa)],[just24]) ).
cnf(c25,plain,
genls('c$utptpcol$u12$u22055','c$utptpcol$u11$u22023'),
inference(clausification,[status(esa)],[just26]) ).
cnf(c27,plain,
genls('c$utptpcol$u13$u22071','c$utptpcol$u12$u22055'),
inference(clausification,[status(esa)],[just28]) ).
cnf(c29,plain,
genls('c$utptpcol$u14$u22072','c$utptpcol$u13$u22071'),
inference(clausification,[status(esa)],[just30]) ).
cnf(c31,plain,
genls('c$utptpcol$u15$u22076','c$utptpcol$u14$u22072'),
inference(clausification,[status(esa)],[just32]) ).
cnf(c33,plain,
genls('c$utptpcol$u2$u65537','c$utptpcol$u1$u65536'),
inference(clausification,[status(esa)],[just34]) ).
cnf(c35,plain,
genls('c$utptpcol$u3$u65538','c$utptpcol$u2$u65537'),
inference(clausification,[status(esa)],[just36]) ).
cnf(c37,plain,
genls('c$utptpcol$u4$u65539','c$utptpcol$u3$u65538'),
inference(clausification,[status(esa)],[just38]) ).
cnf(c39,plain,
genls('c$utptpcol$u5$u69635','c$utptpcol$u4$u65539'),
inference(clausification,[status(esa)],[just40]) ).
cnf(c41,plain,
genls('c$utptpcol$u6$u71683','c$utptpcol$u5$u69635'),
inference(clausification,[status(esa)],[just42]) ).
cnf(c43,plain,
genls('c$utptpcol$u7$u72707','c$utptpcol$u6$u71683'),
inference(clausification,[status(esa)],[just44]) ).
cnf(c45,plain,
genls('c$utptpcol$u8$u72708','c$utptpcol$u7$u72707'),
inference(clausification,[status(esa)],[just46]) ).
cnf(c47,plain,
genls('c$utptpcol$u9$u72709','c$utptpcol$u8$u72708'),
inference(clausification,[status(esa)],[just48]) ).
cnf(c49,plain,
genls('c$utptpcol$u10$u72710','c$utptpcol$u9$u72709'),
inference(clausification,[status(esa)],[just50]) ).
cnf(c51,plain,
genls('c$utptpcol$u11$u72774','c$utptpcol$u10$u72710'),
inference(clausification,[status(esa)],[just52]) ).
cnf(c53,plain,
genls('c$utptpcol$u12$u72775','c$utptpcol$u11$u72774'),
inference(clausification,[status(esa)],[just54]) ).
cnf(c55,plain,
genls('c$utptpcol$u13$u72791','c$utptpcol$u12$u72775'),
inference(clausification,[status(esa)],[just56]) ).
cnf(c57,plain,
genls('c$utptpcol$u14$u72792','c$utptpcol$u13$u72791'),
inference(clausification,[status(esa)],[just58]) ).
cnf(c59,plain,
genls('c$utptpcol$u15$u72793','c$utptpcol$u14$u72792'),
inference(clausification,[status(esa)],[just60]) ).
cnf(c61,plain,
genls('c$utptpcol$u16$u72795','c$utptpcol$u15$u72793'),
inference(clausification,[status(esa)],[just62]) ).
cnf(c63,plain,
disjointwith('c$utptpcol$u1$u1','c$utptpcol$u1$u65536'),
inference(clausification,[status(esa)],[just64]) ).
cnf(c83,plain,
( disjointwith(X0,X2)
| ~ genls(X2,X1)
| ~ disjointwith(X0,X1) ),
inference(clausification,[status(esa)],[just84]) ).
cnf(c84,plain,
( disjointwith(X2,X1)
| ~ genls(X2,X0)
| ~ disjointwith(X0,X1) ),
inference(clausification,[status(esa)],[just85]) ).
cnf(c151,plain,
( genls(X0,X2)
| ~ genls(X1,X2)
| ~ genls(X0,X1) ),
inference(clausification,[status(esa)],[just152]) ).
cnf(c174,plain,
~ disjointwith('c$utptpcol$u15$u22076','c$utptpcol$u16$u72795'),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ genls(X0,'c$utptpcol$u2$u2')
| genls(X0,'c$utptpcol$u1$u1') ),
inference(resolution,[status(thm)],[c151,c5]) ).
cnf(d1,plain,
( ~ genls(X0,'c$utptpcol$u3$u16386')
| genls(X0,'c$utptpcol$u2$u2') ),
inference(resolution,[status(thm)],[c151,c7]) ).
cnf(d2,plain,
( ~ genls(X0,'c$utptpcol$u4$u16387')
| genls(X0,'c$utptpcol$u3$u16386') ),
inference(resolution,[status(thm)],[c151,c9]) ).
cnf(d3,plain,
( ~ genls(X0,'c$utptpcol$u5$u20483')
| genls(X0,'c$utptpcol$u4$u16387') ),
inference(resolution,[status(thm)],[c151,c11]) ).
cnf(d4,plain,
( ~ genls(X0,'c$utptpcol$u6$u20484')
| genls(X0,'c$utptpcol$u5$u20483') ),
inference(resolution,[status(thm)],[c151,c13]) ).
cnf(d5,plain,
( ~ genls(X0,'c$utptpcol$u7$u21508')
| genls(X0,'c$utptpcol$u6$u20484') ),
inference(resolution,[status(thm)],[c151,c15]) ).
cnf(d6,plain,
( ~ genls(X0,'c$utptpcol$u8$u22020')
| genls(X0,'c$utptpcol$u7$u21508') ),
inference(resolution,[status(thm)],[c151,c17]) ).
cnf(d7,plain,
( ~ genls(X0,'c$utptpcol$u9$u22021')
| genls(X0,'c$utptpcol$u8$u22020') ),
inference(resolution,[status(thm)],[c151,c19]) ).
cnf(d8,plain,
( ~ genls(X0,'c$utptpcol$u10$u22022')
| genls(X0,'c$utptpcol$u9$u22021') ),
inference(resolution,[status(thm)],[c151,c21]) ).
cnf(d9,plain,
( ~ genls(X0,'c$utptpcol$u11$u22023')
| genls(X0,'c$utptpcol$u10$u22022') ),
inference(resolution,[status(thm)],[c151,c23]) ).
cnf(d10,plain,
( ~ genls(X0,'c$utptpcol$u12$u22055')
| genls(X0,'c$utptpcol$u11$u22023') ),
inference(resolution,[status(thm)],[c151,c25]) ).
cnf(d11,plain,
( ~ genls(X0,'c$utptpcol$u13$u22071')
| genls(X0,'c$utptpcol$u12$u22055') ),
inference(resolution,[status(thm)],[c151,c27]) ).
cnf(d12,plain,
( ~ genls(X0,'c$utptpcol$u14$u22072')
| genls(X0,'c$utptpcol$u13$u22071') ),
inference(resolution,[status(thm)],[c151,c29]) ).
cnf(d13,plain,
genls('c$utptpcol$u15$u22076','c$utptpcol$u13$u22071'),
inference(resolution,[status(thm)],[d12,c31]) ).
cnf(d14,plain,
genls('c$utptpcol$u15$u22076','c$utptpcol$u12$u22055'),
inference(resolution,[status(thm)],[d13,d11]) ).
cnf(d15,plain,
genls('c$utptpcol$u15$u22076','c$utptpcol$u11$u22023'),
inference(resolution,[status(thm)],[d14,d10]) ).
cnf(d16,plain,
genls('c$utptpcol$u15$u22076','c$utptpcol$u10$u22022'),
inference(resolution,[status(thm)],[d15,d9]) ).
cnf(d17,plain,
genls('c$utptpcol$u15$u22076','c$utptpcol$u9$u22021'),
inference(resolution,[status(thm)],[d16,d8]) ).
cnf(d18,plain,
genls('c$utptpcol$u15$u22076','c$utptpcol$u8$u22020'),
inference(resolution,[status(thm)],[d17,d7]) ).
cnf(d19,plain,
genls('c$utptpcol$u15$u22076','c$utptpcol$u7$u21508'),
inference(resolution,[status(thm)],[d18,d6]) ).
cnf(d20,plain,
genls('c$utptpcol$u15$u22076','c$utptpcol$u6$u20484'),
inference(resolution,[status(thm)],[d19,d5]) ).
cnf(d21,plain,
genls('c$utptpcol$u15$u22076','c$utptpcol$u5$u20483'),
inference(resolution,[status(thm)],[d20,d4]) ).
cnf(d22,plain,
genls('c$utptpcol$u15$u22076','c$utptpcol$u4$u16387'),
inference(resolution,[status(thm)],[d21,d3]) ).
cnf(d23,plain,
genls('c$utptpcol$u15$u22076','c$utptpcol$u3$u16386'),
inference(resolution,[status(thm)],[d22,d2]) ).
cnf(d24,plain,
genls('c$utptpcol$u15$u22076','c$utptpcol$u2$u2'),
inference(resolution,[status(thm)],[d23,d1]) ).
cnf(d25,plain,
genls('c$utptpcol$u15$u22076','c$utptpcol$u1$u1'),
inference(resolution,[status(thm)],[d24,d0]) ).
cnf(d26,plain,
( disjointwith('c$utptpcol$u1$u1',X0)
| ~ genls(X0,'c$utptpcol$u1$u65536') ),
inference(resolution,[status(thm)],[c83,c63]) ).
cnf(d27,plain,
disjointwith('c$utptpcol$u1$u1','c$utptpcol$u2$u65537'),
inference(resolution,[status(thm)],[d26,c33]) ).
cnf(d28,plain,
( disjointwith('c$utptpcol$u1$u1',X0)
| ~ genls(X0,'c$utptpcol$u2$u65537') ),
inference(resolution,[status(thm)],[d27,c83]) ).
cnf(d29,plain,
( ~ genls(X0,'c$utptpcol$u5$u69635')
| genls(X0,'c$utptpcol$u4$u65539') ),
inference(resolution,[status(thm)],[c151,c39]) ).
cnf(d30,plain,
( ~ genls(X0,'c$utptpcol$u6$u71683')
| genls(X0,'c$utptpcol$u5$u69635') ),
inference(resolution,[status(thm)],[c151,c41]) ).
cnf(d31,plain,
( ~ genls(X0,'c$utptpcol$u8$u72708')
| genls(X0,'c$utptpcol$u7$u72707') ),
inference(resolution,[status(thm)],[c151,c45]) ).
cnf(d32,plain,
( ~ genls(X0,'c$utptpcol$u9$u72709')
| genls(X0,'c$utptpcol$u8$u72708') ),
inference(resolution,[status(thm)],[c151,c47]) ).
cnf(d33,plain,
( ~ genls(X0,'c$utptpcol$u10$u72710')
| genls(X0,'c$utptpcol$u9$u72709') ),
inference(resolution,[status(thm)],[c151,c49]) ).
cnf(d34,plain,
( ~ genls(X0,'c$utptpcol$u11$u72774')
| genls(X0,'c$utptpcol$u10$u72710') ),
inference(resolution,[status(thm)],[c151,c51]) ).
cnf(d35,plain,
( ~ genls(X0,'c$utptpcol$u12$u72775')
| genls(X0,'c$utptpcol$u11$u72774') ),
inference(resolution,[status(thm)],[c151,c53]) ).
cnf(d36,plain,
( ~ genls(X0,'c$utptpcol$u13$u72791')
| genls(X0,'c$utptpcol$u12$u72775') ),
inference(resolution,[status(thm)],[c151,c55]) ).
cnf(d37,plain,
( ~ genls(X0,'c$utptpcol$u14$u72792')
| genls(X0,'c$utptpcol$u13$u72791') ),
inference(resolution,[status(thm)],[c151,c57]) ).
cnf(d38,plain,
( ~ genls(X0,'c$utptpcol$u15$u72793')
| genls(X0,'c$utptpcol$u14$u72792') ),
inference(resolution,[status(thm)],[c151,c59]) ).
cnf(d39,plain,
genls('c$utptpcol$u16$u72795','c$utptpcol$u14$u72792'),
inference(resolution,[status(thm)],[d38,c61]) ).
cnf(d40,plain,
genls('c$utptpcol$u16$u72795','c$utptpcol$u13$u72791'),
inference(resolution,[status(thm)],[d39,d37]) ).
cnf(d41,plain,
genls('c$utptpcol$u16$u72795','c$utptpcol$u12$u72775'),
inference(resolution,[status(thm)],[d40,d36]) ).
cnf(d42,plain,
genls('c$utptpcol$u16$u72795','c$utptpcol$u11$u72774'),
inference(resolution,[status(thm)],[d41,d35]) ).
cnf(d43,plain,
genls('c$utptpcol$u16$u72795','c$utptpcol$u10$u72710'),
inference(resolution,[status(thm)],[d42,d34]) ).
cnf(d44,plain,
genls('c$utptpcol$u16$u72795','c$utptpcol$u9$u72709'),
inference(resolution,[status(thm)],[d43,d33]) ).
cnf(d45,plain,
genls('c$utptpcol$u16$u72795','c$utptpcol$u8$u72708'),
inference(resolution,[status(thm)],[d44,d32]) ).
cnf(d46,plain,
genls('c$utptpcol$u16$u72795','c$utptpcol$u7$u72707'),
inference(resolution,[status(thm)],[d45,d31]) ).
cnf(d47,plain,
( ~ genls(X0,'c$utptpcol$u7$u72707')
| genls(X0,'c$utptpcol$u6$u71683') ),
inference(resolution,[status(thm)],[c151,c43]) ).
cnf(d48,plain,
genls('c$utptpcol$u16$u72795','c$utptpcol$u6$u71683'),
inference(resolution,[status(thm)],[d47,d46]) ).
cnf(d49,plain,
genls('c$utptpcol$u16$u72795','c$utptpcol$u5$u69635'),
inference(resolution,[status(thm)],[d48,d30]) ).
cnf(d50,plain,
genls('c$utptpcol$u16$u72795','c$utptpcol$u4$u65539'),
inference(resolution,[status(thm)],[d49,d29]) ).
cnf(d51,plain,
( ~ genls(X0,'c$utptpcol$u4$u65539')
| genls(X0,'c$utptpcol$u3$u65538') ),
inference(resolution,[status(thm)],[c151,c37]) ).
cnf(d52,plain,
genls('c$utptpcol$u16$u72795','c$utptpcol$u3$u65538'),
inference(resolution,[status(thm)],[d51,d50]) ).
cnf(d53,plain,
( ~ genls(X0,'c$utptpcol$u3$u65538')
| genls(X0,'c$utptpcol$u2$u65537') ),
inference(resolution,[status(thm)],[c151,c35]) ).
cnf(d54,plain,
genls('c$utptpcol$u16$u72795','c$utptpcol$u2$u65537'),
inference(resolution,[status(thm)],[d53,d52]) ).
cnf(d55,plain,
disjointwith('c$utptpcol$u1$u1','c$utptpcol$u16$u72795'),
inference(resolution,[status(thm)],[d54,d28]) ).
cnf(d56,plain,
( disjointwith(X0,'c$utptpcol$u16$u72795')
| ~ genls(X0,'c$utptpcol$u1$u1') ),
inference(resolution,[status(thm)],[d55,c84]) ).
cnf(d57,plain,
disjointwith('c$utptpcol$u15$u22076','c$utptpcol$u16$u72795'),
inference(resolution,[status(thm)],[d56,d25]) ).
cnf(d58,plain,
$false,
inference(resolution,[status(thm)],[c174,d57]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR036+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.10/0.36 % Computer : n026.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 00:09:11 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 42.55/5.83 % SZS status Theorem for theBenchmark.p
% 42.55/5.83 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------