%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR049+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:59 AM UTC 2026
% Result : Theorem 42.21s 10.30s
% Output : CNFRefutation 42.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 35
% Syntax : Number of formulae : 132 ( 94 unt; 0 def)
% Number of atoms : 176 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 82 ( 38 ~; 36 |; 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 : 33 ( 33 usr; 33 con; 0-0 aty)
% Number of variables : 48 ( 0 sgn 9 !; 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$u24578','c$utptpcol$u3$u16386') ).
fof(just13,axiom,
genls('c$utptpcol$u5$u24579','c$utptpcol$u4$u24578') ).
fof(just15,axiom,
genls('c$utptpcol$u6$u26627','c$utptpcol$u5$u24579') ).
fof(just17,axiom,
genls('c$utptpcol$u7$u26628','c$utptpcol$u6$u26627') ).
fof(just19,axiom,
genls('c$utptpcol$u8$u26629','c$utptpcol$u7$u26628') ).
fof(just21,axiom,
genls('c$utptpcol$u9$u26885','c$utptpcol$u8$u26629') ).
fof(just23,axiom,
genls('c$utptpcol$u10$u26886','c$utptpcol$u9$u26885') ).
fof(just25,axiom,
genls('c$utptpcol$u11$u26887','c$utptpcol$u10$u26886') ).
fof(just27,axiom,
genls('c$utptpcol$u12$u26919','c$utptpcol$u11$u26887') ).
fof(just29,axiom,
genls('c$utptpcol$u13$u26920','c$utptpcol$u12$u26919') ).
fof(just31,axiom,
genls('c$utptpcol$u14$u26921','c$utptpcol$u13$u26920') ).
fof(just33,axiom,
genls('c$utptpcol$u15$u26925','c$utptpcol$u14$u26921') ).
fof(just35,axiom,
genls('c$utptpcol$u16$u26926','c$utptpcol$u15$u26925') ).
fof(just37,axiom,
genls('c$utptpcol$u2$u65537','c$utptpcol$u1$u65536') ).
fof(just39,axiom,
genls('c$utptpcol$u3$u81921','c$utptpcol$u2$u65537') ).
fof(just41,axiom,
genls('c$utptpcol$u4$u90113','c$utptpcol$u3$u81921') ).
fof(just43,axiom,
genls('c$utptpcol$u5$u90114','c$utptpcol$u4$u90113') ).
fof(just45,axiom,
genls('c$utptpcol$u6$u92162','c$utptpcol$u5$u90114') ).
fof(just47,axiom,
genls('c$utptpcol$u7$u92163','c$utptpcol$u6$u92162') ).
fof(just49,axiom,
genls('c$utptpcol$u8$u92164','c$utptpcol$u7$u92163') ).
fof(just51,axiom,
genls('c$utptpcol$u9$u92165','c$utptpcol$u8$u92164') ).
fof(just53,axiom,
genls('c$utptpcol$u10$u92166','c$utptpcol$u9$u92165') ).
fof(just55,axiom,
genls('c$utptpcol$u11$u92230','c$utptpcol$u10$u92166') ).
fof(just57,axiom,
genls('c$utptpcol$u12$u92262','c$utptpcol$u11$u92230') ).
fof(just59,axiom,
genls('c$utptpcol$u13$u92263','c$utptpcol$u12$u92262') ).
fof(just61,axiom,
genls('c$utptpcol$u14$u92264','c$utptpcol$u13$u92263') ).
fof(just63,axiom,
genls('c$utptpcol$u15$u92268','c$utptpcol$u14$u92264') ).
fof(just65,axiom,
genls('c$utptpcol$u16$u92269','c$utptpcol$u15$u92268') ).
fof(just67,axiom,
disjointwith('c$utptpcol$u1$u1','c$utptpcol$u1$u65536') ).
fof(just85,axiom,
! [X0,X1,X2] :
( ( genls(X2,X1)
& disjointwith(X0,X1) )
=> disjointwith(X0,X2) ) ).
fof(just86,axiom,
! [X0,X1,X2] :
( ( genls(X2,X0)
& disjointwith(X0,X1) )
=> disjointwith(X2,X1) ) ).
fof(just155,axiom,
! [X0,X1,X2] :
( ( genls(X1,X2)
& genls(X0,X1) )
=> genls(X0,X2) ) ).
fof(query49,conjecture,
( mtvisible('c$uunitedstatesgeographypeoplemt')
=> disjointwith('c$utptpcol$u16$u26926','c$utptpcol$u16$u92269') ) ).
fof(negated_conjecture,negated_conjecture,
~ ( mtvisible('c$uunitedstatesgeographypeoplemt')
=> disjointwith('c$utptpcol$u16$u26926','c$utptpcol$u16$u92269') ),
inference(negate_conjecture,[status(cth)],[query49]) ).
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$u24578','c$utptpcol$u3$u16386'),
inference(clausification,[status(esa)],[just11]) ).
cnf(c12,plain,
genls('c$utptpcol$u5$u24579','c$utptpcol$u4$u24578'),
inference(clausification,[status(esa)],[just13]) ).
cnf(c14,plain,
genls('c$utptpcol$u6$u26627','c$utptpcol$u5$u24579'),
inference(clausification,[status(esa)],[just15]) ).
cnf(c16,plain,
genls('c$utptpcol$u7$u26628','c$utptpcol$u6$u26627'),
inference(clausification,[status(esa)],[just17]) ).
cnf(c18,plain,
genls('c$utptpcol$u8$u26629','c$utptpcol$u7$u26628'),
inference(clausification,[status(esa)],[just19]) ).
cnf(c20,plain,
genls('c$utptpcol$u9$u26885','c$utptpcol$u8$u26629'),
inference(clausification,[status(esa)],[just21]) ).
cnf(c22,plain,
genls('c$utptpcol$u10$u26886','c$utptpcol$u9$u26885'),
inference(clausification,[status(esa)],[just23]) ).
cnf(c24,plain,
genls('c$utptpcol$u11$u26887','c$utptpcol$u10$u26886'),
inference(clausification,[status(esa)],[just25]) ).
cnf(c26,plain,
genls('c$utptpcol$u12$u26919','c$utptpcol$u11$u26887'),
inference(clausification,[status(esa)],[just27]) ).
cnf(c28,plain,
genls('c$utptpcol$u13$u26920','c$utptpcol$u12$u26919'),
inference(clausification,[status(esa)],[just29]) ).
cnf(c30,plain,
genls('c$utptpcol$u14$u26921','c$utptpcol$u13$u26920'),
inference(clausification,[status(esa)],[just31]) ).
cnf(c32,plain,
genls('c$utptpcol$u15$u26925','c$utptpcol$u14$u26921'),
inference(clausification,[status(esa)],[just33]) ).
cnf(c34,plain,
genls('c$utptpcol$u16$u26926','c$utptpcol$u15$u26925'),
inference(clausification,[status(esa)],[just35]) ).
cnf(c36,plain,
genls('c$utptpcol$u2$u65537','c$utptpcol$u1$u65536'),
inference(clausification,[status(esa)],[just37]) ).
cnf(c38,plain,
genls('c$utptpcol$u3$u81921','c$utptpcol$u2$u65537'),
inference(clausification,[status(esa)],[just39]) ).
cnf(c40,plain,
genls('c$utptpcol$u4$u90113','c$utptpcol$u3$u81921'),
inference(clausification,[status(esa)],[just41]) ).
cnf(c42,plain,
genls('c$utptpcol$u5$u90114','c$utptpcol$u4$u90113'),
inference(clausification,[status(esa)],[just43]) ).
cnf(c44,plain,
genls('c$utptpcol$u6$u92162','c$utptpcol$u5$u90114'),
inference(clausification,[status(esa)],[just45]) ).
cnf(c46,plain,
genls('c$utptpcol$u7$u92163','c$utptpcol$u6$u92162'),
inference(clausification,[status(esa)],[just47]) ).
cnf(c48,plain,
genls('c$utptpcol$u8$u92164','c$utptpcol$u7$u92163'),
inference(clausification,[status(esa)],[just49]) ).
cnf(c50,plain,
genls('c$utptpcol$u9$u92165','c$utptpcol$u8$u92164'),
inference(clausification,[status(esa)],[just51]) ).
cnf(c52,plain,
genls('c$utptpcol$u10$u92166','c$utptpcol$u9$u92165'),
inference(clausification,[status(esa)],[just53]) ).
cnf(c54,plain,
genls('c$utptpcol$u11$u92230','c$utptpcol$u10$u92166'),
inference(clausification,[status(esa)],[just55]) ).
cnf(c56,plain,
genls('c$utptpcol$u12$u92262','c$utptpcol$u11$u92230'),
inference(clausification,[status(esa)],[just57]) ).
cnf(c58,plain,
genls('c$utptpcol$u13$u92263','c$utptpcol$u12$u92262'),
inference(clausification,[status(esa)],[just59]) ).
cnf(c60,plain,
genls('c$utptpcol$u14$u92264','c$utptpcol$u13$u92263'),
inference(clausification,[status(esa)],[just61]) ).
cnf(c62,plain,
genls('c$utptpcol$u15$u92268','c$utptpcol$u14$u92264'),
inference(clausification,[status(esa)],[just63]) ).
cnf(c64,plain,
genls('c$utptpcol$u16$u92269','c$utptpcol$u15$u92268'),
inference(clausification,[status(esa)],[just65]) ).
cnf(c66,plain,
disjointwith('c$utptpcol$u1$u1','c$utptpcol$u1$u65536'),
inference(clausification,[status(esa)],[just67]) ).
cnf(c84,plain,
( disjointwith(X0,X2)
| ~ genls(X2,X1)
| ~ disjointwith(X0,X1) ),
inference(clausification,[status(esa)],[just85]) ).
cnf(c85,plain,
( disjointwith(X2,X1)
| ~ genls(X2,X0)
| ~ disjointwith(X0,X1) ),
inference(clausification,[status(esa)],[just86]) ).
cnf(c154,plain,
( genls(X0,X2)
| ~ genls(X1,X2)
| ~ genls(X0,X1) ),
inference(clausification,[status(esa)],[just155]) ).
cnf(c177,plain,
~ disjointwith('c$utptpcol$u16$u26926','c$utptpcol$u16$u92269'),
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)],[c154,c6]) ).
cnf(d1,plain,
( ~ genls(X0,'c$utptpcol$u3$u16386')
| genls(X0,'c$utptpcol$u2$u2') ),
inference(resolution,[status(thm)],[c154,c8]) ).
cnf(d2,plain,
( ~ genls(X0,'c$utptpcol$u4$u24578')
| genls(X0,'c$utptpcol$u3$u16386') ),
inference(resolution,[status(thm)],[c154,c10]) ).
cnf(d3,plain,
( ~ genls(X0,'c$utptpcol$u5$u24579')
| genls(X0,'c$utptpcol$u4$u24578') ),
inference(resolution,[status(thm)],[c154,c12]) ).
cnf(d4,plain,
( ~ genls(X0,'c$utptpcol$u6$u26627')
| genls(X0,'c$utptpcol$u5$u24579') ),
inference(resolution,[status(thm)],[c154,c14]) ).
cnf(d5,plain,
( ~ genls(X0,'c$utptpcol$u7$u26628')
| genls(X0,'c$utptpcol$u6$u26627') ),
inference(resolution,[status(thm)],[c154,c16]) ).
cnf(d6,plain,
( ~ genls(X0,'c$utptpcol$u8$u26629')
| genls(X0,'c$utptpcol$u7$u26628') ),
inference(resolution,[status(thm)],[c154,c18]) ).
cnf(d7,plain,
( ~ genls(X0,'c$utptpcol$u9$u26885')
| genls(X0,'c$utptpcol$u8$u26629') ),
inference(resolution,[status(thm)],[c154,c20]) ).
cnf(d8,plain,
( ~ genls(X0,'c$utptpcol$u10$u26886')
| genls(X0,'c$utptpcol$u9$u26885') ),
inference(resolution,[status(thm)],[c154,c22]) ).
cnf(d9,plain,
( ~ genls(X0,'c$utptpcol$u11$u26887')
| genls(X0,'c$utptpcol$u10$u26886') ),
inference(resolution,[status(thm)],[c154,c24]) ).
cnf(d10,plain,
( ~ genls(X0,'c$utptpcol$u12$u26919')
| genls(X0,'c$utptpcol$u11$u26887') ),
inference(resolution,[status(thm)],[c154,c26]) ).
cnf(d11,plain,
( ~ genls(X0,'c$utptpcol$u13$u26920')
| genls(X0,'c$utptpcol$u12$u26919') ),
inference(resolution,[status(thm)],[c154,c28]) ).
cnf(d12,plain,
( ~ genls(X0,'c$utptpcol$u14$u26921')
| genls(X0,'c$utptpcol$u13$u26920') ),
inference(resolution,[status(thm)],[c154,c30]) ).
cnf(d13,plain,
( ~ genls(X0,'c$utptpcol$u15$u26925')
| genls(X0,'c$utptpcol$u14$u26921') ),
inference(resolution,[status(thm)],[c154,c32]) ).
cnf(d14,plain,
genls('c$utptpcol$u16$u26926','c$utptpcol$u14$u26921'),
inference(resolution,[status(thm)],[d13,c34]) ).
cnf(d15,plain,
genls('c$utptpcol$u16$u26926','c$utptpcol$u13$u26920'),
inference(resolution,[status(thm)],[d14,d12]) ).
cnf(d16,plain,
genls('c$utptpcol$u16$u26926','c$utptpcol$u12$u26919'),
inference(resolution,[status(thm)],[d15,d11]) ).
cnf(d17,plain,
genls('c$utptpcol$u16$u26926','c$utptpcol$u11$u26887'),
inference(resolution,[status(thm)],[d16,d10]) ).
cnf(d18,plain,
genls('c$utptpcol$u16$u26926','c$utptpcol$u10$u26886'),
inference(resolution,[status(thm)],[d17,d9]) ).
cnf(d19,plain,
genls('c$utptpcol$u16$u26926','c$utptpcol$u9$u26885'),
inference(resolution,[status(thm)],[d18,d8]) ).
cnf(d20,plain,
genls('c$utptpcol$u16$u26926','c$utptpcol$u8$u26629'),
inference(resolution,[status(thm)],[d19,d7]) ).
cnf(d21,plain,
genls('c$utptpcol$u16$u26926','c$utptpcol$u7$u26628'),
inference(resolution,[status(thm)],[d20,d6]) ).
cnf(d22,plain,
genls('c$utptpcol$u16$u26926','c$utptpcol$u6$u26627'),
inference(resolution,[status(thm)],[d21,d5]) ).
cnf(d23,plain,
genls('c$utptpcol$u16$u26926','c$utptpcol$u5$u24579'),
inference(resolution,[status(thm)],[d22,d4]) ).
cnf(d24,plain,
genls('c$utptpcol$u16$u26926','c$utptpcol$u4$u24578'),
inference(resolution,[status(thm)],[d23,d3]) ).
cnf(d25,plain,
genls('c$utptpcol$u16$u26926','c$utptpcol$u3$u16386'),
inference(resolution,[status(thm)],[d24,d2]) ).
cnf(d26,plain,
genls('c$utptpcol$u16$u26926','c$utptpcol$u2$u2'),
inference(resolution,[status(thm)],[d25,d1]) ).
cnf(d27,plain,
genls('c$utptpcol$u16$u26926','c$utptpcol$u1$u1'),
inference(resolution,[status(thm)],[d26,d0]) ).
cnf(d28,plain,
( disjointwith('c$utptpcol$u1$u1',X0)
| ~ genls(X0,'c$utptpcol$u1$u65536') ),
inference(resolution,[status(thm)],[c84,c66]) ).
cnf(d29,plain,
( ~ genls(X0,'c$utptpcol$u2$u65537')
| genls(X0,'c$utptpcol$u1$u65536') ),
inference(resolution,[status(thm)],[c154,c36]) ).
cnf(d30,plain,
( ~ genls(X0,'c$utptpcol$u3$u81921')
| genls(X0,'c$utptpcol$u2$u65537') ),
inference(resolution,[status(thm)],[c154,c38]) ).
cnf(d31,plain,
( ~ genls(X0,'c$utptpcol$u4$u90113')
| genls(X0,'c$utptpcol$u3$u81921') ),
inference(resolution,[status(thm)],[c154,c40]) ).
cnf(d32,plain,
( ~ genls(X0,'c$utptpcol$u5$u90114')
| genls(X0,'c$utptpcol$u4$u90113') ),
inference(resolution,[status(thm)],[c154,c42]) ).
cnf(d33,plain,
( ~ genls(X0,'c$utptpcol$u6$u92162')
| genls(X0,'c$utptpcol$u5$u90114') ),
inference(resolution,[status(thm)],[c154,c44]) ).
cnf(d34,plain,
( ~ genls(X0,'c$utptpcol$u7$u92163')
| genls(X0,'c$utptpcol$u6$u92162') ),
inference(resolution,[status(thm)],[c154,c46]) ).
cnf(d35,plain,
( ~ genls(X0,'c$utptpcol$u8$u92164')
| genls(X0,'c$utptpcol$u7$u92163') ),
inference(resolution,[status(thm)],[c154,c48]) ).
cnf(d36,plain,
( ~ genls(X0,'c$utptpcol$u9$u92165')
| genls(X0,'c$utptpcol$u8$u92164') ),
inference(resolution,[status(thm)],[c154,c50]) ).
cnf(d37,plain,
( ~ genls(X0,'c$utptpcol$u10$u92166')
| genls(X0,'c$utptpcol$u9$u92165') ),
inference(resolution,[status(thm)],[c154,c52]) ).
cnf(d38,plain,
( ~ genls(X0,'c$utptpcol$u11$u92230')
| genls(X0,'c$utptpcol$u10$u92166') ),
inference(resolution,[status(thm)],[c154,c54]) ).
cnf(d39,plain,
( ~ genls(X0,'c$utptpcol$u12$u92262')
| genls(X0,'c$utptpcol$u11$u92230') ),
inference(resolution,[status(thm)],[c154,c56]) ).
cnf(d40,plain,
( ~ genls(X0,'c$utptpcol$u13$u92263')
| genls(X0,'c$utptpcol$u12$u92262') ),
inference(resolution,[status(thm)],[c154,c58]) ).
cnf(d41,plain,
( ~ genls(X0,'c$utptpcol$u14$u92264')
| genls(X0,'c$utptpcol$u13$u92263') ),
inference(resolution,[status(thm)],[c154,c60]) ).
cnf(d42,plain,
( ~ genls(X0,'c$utptpcol$u15$u92268')
| genls(X0,'c$utptpcol$u14$u92264') ),
inference(resolution,[status(thm)],[c154,c62]) ).
cnf(d43,plain,
genls('c$utptpcol$u16$u92269','c$utptpcol$u14$u92264'),
inference(resolution,[status(thm)],[d42,c64]) ).
cnf(d44,plain,
genls('c$utptpcol$u16$u92269','c$utptpcol$u13$u92263'),
inference(resolution,[status(thm)],[d43,d41]) ).
cnf(d45,plain,
genls('c$utptpcol$u16$u92269','c$utptpcol$u12$u92262'),
inference(resolution,[status(thm)],[d44,d40]) ).
cnf(d46,plain,
genls('c$utptpcol$u16$u92269','c$utptpcol$u11$u92230'),
inference(resolution,[status(thm)],[d45,d39]) ).
cnf(d47,plain,
genls('c$utptpcol$u16$u92269','c$utptpcol$u10$u92166'),
inference(resolution,[status(thm)],[d46,d38]) ).
cnf(d48,plain,
genls('c$utptpcol$u16$u92269','c$utptpcol$u9$u92165'),
inference(resolution,[status(thm)],[d47,d37]) ).
cnf(d49,plain,
genls('c$utptpcol$u16$u92269','c$utptpcol$u8$u92164'),
inference(resolution,[status(thm)],[d48,d36]) ).
cnf(d50,plain,
genls('c$utptpcol$u16$u92269','c$utptpcol$u7$u92163'),
inference(resolution,[status(thm)],[d49,d35]) ).
cnf(d51,plain,
genls('c$utptpcol$u16$u92269','c$utptpcol$u6$u92162'),
inference(resolution,[status(thm)],[d50,d34]) ).
cnf(d52,plain,
genls('c$utptpcol$u16$u92269','c$utptpcol$u5$u90114'),
inference(resolution,[status(thm)],[d51,d33]) ).
cnf(d53,plain,
genls('c$utptpcol$u16$u92269','c$utptpcol$u4$u90113'),
inference(resolution,[status(thm)],[d52,d32]) ).
cnf(d54,plain,
genls('c$utptpcol$u16$u92269','c$utptpcol$u3$u81921'),
inference(resolution,[status(thm)],[d53,d31]) ).
cnf(d55,plain,
genls('c$utptpcol$u16$u92269','c$utptpcol$u2$u65537'),
inference(resolution,[status(thm)],[d54,d30]) ).
cnf(d56,plain,
genls('c$utptpcol$u16$u92269','c$utptpcol$u1$u65536'),
inference(resolution,[status(thm)],[d55,d29]) ).
cnf(d57,plain,
disjointwith('c$utptpcol$u1$u1','c$utptpcol$u16$u92269'),
inference(resolution,[status(thm)],[d56,d28]) ).
cnf(d58,plain,
( disjointwith(X0,'c$utptpcol$u16$u92269')
| ~ genls(X0,'c$utptpcol$u1$u1') ),
inference(resolution,[status(thm)],[d57,c85]) ).
cnf(d59,plain,
disjointwith('c$utptpcol$u16$u26926','c$utptpcol$u16$u92269'),
inference(resolution,[status(thm)],[d58,d27]) ).
cnf(d60,plain,
$false,
inference(resolution,[status(thm)],[c177,d59]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR049+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.42 % Computer : n019.cluster.edu
% 0.14/0.42 % Model : x86_64 x86_64
% 0.14/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.42 % Memory : 8046.5625MB
% 0.14/0.42 % OS : Linux 6.8.0-71-generic
% 0.14/0.42 % CPULimit : 300
% 0.14/0.42 % WCLimit : 300
% 0.14/0.42 % DateTime : Sun Sep 27 00:18:18 UTC 2026
% 0.14/0.42 % CPUTime :
% 0.14/0.42 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 42.21/10.30 % SZS status Theorem for theBenchmark.p
% 42.21/10.30 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------