%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SYN704-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n029.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Thu Jul 21 09:04:53 EDT 2022
% Result : Unsatisfiable 0.91s 1.12s
% Output : CNFRefutation 0.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 14
% Syntax : Number of clauses : 65 ( 29 unt; 0 nHn; 46 RR)
% Number of literals : 123 ( 0 equ; 60 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 11 con; 0-2 aty)
% Number of variables : 103 ( 5 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(p7_3,negated_conjecture,
p7(X162,X162) ).
cnf(p6_4,negated_conjecture,
p6(X155,X155) ).
cnf(p4_8,negated_conjecture,
p4(X119,X119) ).
cnf(p2_20,negated_conjecture,
p2(X38,X38) ).
cnf(p7_26,negated_conjecture,
p7(c54,c55) ).
cnf(p7_29,negated_conjecture,
( p7(X163,X164)
| ~ p7(X162,X163)
| ~ p7(X162,X164) ) ).
cnf(p3_40,negated_conjecture,
( p3(X78,X79)
| ~ p3(X77,X78)
| ~ p3(X77,X79) ) ).
cnf(not_p47_52,negated_conjecture,
~ p47(f20(f22(f24(f26(c56,X65),X66),X67),X68),X68) ).
cnf(p47_53,negated_conjecture,
( p47(X151,X152)
| ~ p47(X153,X154)
| ~ p7(X154,X152)
| ~ p4(X153,X151) ) ).
cnf(p4_58,negated_conjecture,
( p4(f5(X126,X127),f5(X128,X129))
| ~ p2(X126,X128)
| ~ p3(X127,X129) ) ).
cnf(p3_64,negated_conjecture,
( p3(f8(X84,X85),f8(X86,X87))
| ~ p6(X84,X86)
| ~ p7(X85,X87) ) ).
cnf(p47_74,negated_conjecture,
( p47(X147,X148)
| ~ p47(f5(c48,f13(f16(f18(c50,X147),X149),X150)),X148) ) ).
cnf(p47_77,negated_conjecture,
p47(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54)),c55) ).
cnf(p3_80,negated_conjecture,
p3(f8(f10(c49,f13(f16(f18(c50,X65),X66),X67)),X68),f13(f16(f18(c50,f20(f22(f24(f26(c56,X65),X66),X67),X68)),f30(f32(f34(f36(c57,X65),X66),X67),X68)),f40(f42(f44(f46(c58,X65),X66),X67),X68))) ).
cnf(refute_0_0,plain,
p4(X_2510,X_2510),
inference(subst,[],[p4_8:[bind(X119,$fot(X_2510))]]) ).
cnf(refute_0_1,plain,
p7(c54,c54),
inference(subst,[],[p7_3:[bind(X162,$fot(c54))]]) ).
cnf(refute_0_2,plain,
( ~ p7(c54,X_41)
| ~ p7(c54,c55)
| p7(c55,X_41) ),
inference(subst,[],[p7_29:[bind(X162,$fot(c54)),bind(X163,$fot(c55)),bind(X164,$fot(X_41))]]) ).
cnf(refute_0_3,plain,
( ~ p7(c54,X_41)
| p7(c55,X_41) ),
inference(resolve,[$cnf( p7(c54,c55) )],[p7_26,refute_0_2]) ).
cnf(refute_0_4,plain,
( ~ p7(c54,c54)
| p7(c55,c54) ),
inference(subst,[],[refute_0_3:[bind(X_41,$fot(c54))]]) ).
cnf(refute_0_5,plain,
p7(c55,c54),
inference(resolve,[$cnf( p7(c54,c54) )],[refute_0_1,refute_0_4]) ).
cnf(refute_0_6,plain,
( ~ p4(X_2497,X_2495)
| ~ p47(X_2497,c55)
| ~ p7(c55,c54)
| p47(X_2495,c54) ),
inference(subst,[],[p47_53:[bind(X151,$fot(X_2495)),bind(X152,$fot(c54)),bind(X153,$fot(X_2497)),bind(X154,$fot(c55))]]) ).
cnf(refute_0_7,plain,
( ~ p4(X_2497,X_2495)
| ~ p47(X_2497,c55)
| p47(X_2495,c54) ),
inference(resolve,[$cnf( p7(c55,c54) )],[refute_0_5,refute_0_6]) ).
cnf(refute_0_8,plain,
( ~ p4(X_2510,X_2510)
| ~ p47(X_2510,c55)
| p47(X_2510,c54) ),
inference(subst,[],[refute_0_7:[bind(X_2495,$fot(X_2510)),bind(X_2497,$fot(X_2510))]]) ).
cnf(refute_0_9,plain,
( ~ p47(X_2510,c55)
| p47(X_2510,c54) ),
inference(resolve,[$cnf( p4(X_2510,X_2510) )],[refute_0_0,refute_0_8]) ).
cnf(refute_0_10,plain,
( ~ p47(f20(f22(f24(f26(c56,c51),c52),c53),c54),c55)
| p47(f20(f22(f24(f26(c56,c51),c52),c53),c54),c54) ),
inference(subst,[],[refute_0_9:[bind(X_2510,$fot(f20(f22(f24(f26(c56,c51),c52),c53),c54)))]]) ).
cnf(refute_0_11,plain,
( ~ p47(f5(c48,f13(f16(f18(c50,f20(f22(f24(f26(c56,c51),c52),c53),c54)),f30(f32(f34(f36(c57,c51),c52),c53),c54)),f40(f42(f44(f46(c58,c51),c52),c53),c54))),c55)
| p47(f20(f22(f24(f26(c56,c51),c52),c53),c54),c55) ),
inference(subst,[],[p47_74:[bind(X147,$fot(f20(f22(f24(f26(c56,c51),c52),c53),c54))),bind(X148,$fot(c55)),bind(X149,$fot(f30(f32(f34(f36(c57,c51),c52),c53),c54))),bind(X150,$fot(f40(f42(f44(f46(c58,c51),c52),c53),c54)))]]) ).
cnf(refute_0_12,plain,
p2(X_219,X_219),
inference(subst,[],[p2_20:[bind(X38,$fot(X_219))]]) ).
cnf(refute_0_13,plain,
( ~ p2(X_219,X_219)
| ~ p3(X_218,X_220)
| p4(f5(X_219,X_218),f5(X_219,X_220)) ),
inference(subst,[],[p4_58:[bind(X126,$fot(X_219)),bind(X127,$fot(X_218)),bind(X128,$fot(X_219)),bind(X129,$fot(X_220))]]) ).
cnf(refute_0_14,plain,
( ~ p3(X_218,X_220)
| p4(f5(X_219,X_218),f5(X_219,X_220)) ),
inference(resolve,[$cnf( p2(X_219,X_219) )],[refute_0_12,refute_0_13]) ).
cnf(refute_0_15,plain,
( ~ p3(f8(f10(c49,f13(f16(f18(c50,X_2228),X_2229),X_2230)),c55),f13(f16(f18(c50,f20(f22(f24(f26(c56,X_2228),X_2229),X_2230),c54)),f30(f32(f34(f36(c57,X_2228),X_2229),X_2230),c54)),f40(f42(f44(f46(c58,X_2228),X_2229),X_2230),c54)))
| p4(f5(X_219,f8(f10(c49,f13(f16(f18(c50,X_2228),X_2229),X_2230)),c55)),f5(X_219,f13(f16(f18(c50,f20(f22(f24(f26(c56,X_2228),X_2229),X_2230),c54)),f30(f32(f34(f36(c57,X_2228),X_2229),X_2230),c54)),f40(f42(f44(f46(c58,X_2228),X_2229),X_2230),c54)))) ),
inference(subst,[],[refute_0_14:[bind(X_218,$fot(f8(f10(c49,f13(f16(f18(c50,X_2228),X_2229),X_2230)),c55))),bind(X_220,$fot(f13(f16(f18(c50,f20(f22(f24(f26(c56,X_2228),X_2229),X_2230),c54)),f30(f32(f34(f36(c57,X_2228),X_2229),X_2230),c54)),f40(f42(f44(f46(c58,X_2228),X_2229),X_2230),c54))))]]) ).
cnf(refute_0_16,plain,
( ~ p3(f8(X_371,c54),X79)
| ~ p3(f8(X_371,c54),f8(X_371,c55))
| p3(f8(X_371,c55),X79) ),
inference(subst,[],[p3_40:[bind(X77,$fot(f8(X_371,c54))),bind(X78,$fot(f8(X_371,c55)))]]) ).
cnf(refute_0_17,plain,
p6(X_370,X_370),
inference(subst,[],[p6_4:[bind(X155,$fot(X_370))]]) ).
cnf(refute_0_18,plain,
( ~ p6(X_365,X_367)
| ~ p7(c54,c55)
| p3(f8(X_365,c54),f8(X_367,c55)) ),
inference(subst,[],[p3_64:[bind(X84,$fot(X_365)),bind(X85,$fot(c54)),bind(X86,$fot(X_367)),bind(X87,$fot(c55))]]) ).
cnf(refute_0_19,plain,
( ~ p6(X_365,X_367)
| p3(f8(X_365,c54),f8(X_367,c55)) ),
inference(resolve,[$cnf( p7(c54,c55) )],[p7_26,refute_0_18]) ).
cnf(refute_0_20,plain,
( ~ p6(X_370,X_370)
| p3(f8(X_370,c54),f8(X_370,c55)) ),
inference(subst,[],[refute_0_19:[bind(X_365,$fot(X_370)),bind(X_367,$fot(X_370))]]) ).
cnf(refute_0_21,plain,
p3(f8(X_370,c54),f8(X_370,c55)),
inference(resolve,[$cnf( p6(X_370,X_370) )],[refute_0_17,refute_0_20]) ).
cnf(refute_0_22,plain,
p3(f8(X_371,c54),f8(X_371,c55)),
inference(subst,[],[refute_0_21:[bind(X_370,$fot(X_371))]]) ).
cnf(refute_0_23,plain,
( ~ p3(f8(X_371,c54),X79)
| p3(f8(X_371,c55),X79) ),
inference(resolve,[$cnf( p3(f8(X_371,c54),f8(X_371,c55)) )],[refute_0_22,refute_0_16]) ).
cnf(refute_0_24,plain,
( ~ p3(f8(f10(c49,f13(f16(f18(c50,X_1728),X_1729),X_1730)),c54),f13(f16(f18(c50,f20(f22(f24(f26(c56,X_1728),X_1729),X_1730),c54)),f30(f32(f34(f36(c57,X_1728),X_1729),X_1730),c54)),f40(f42(f44(f46(c58,X_1728),X_1729),X_1730),c54)))
| p3(f8(f10(c49,f13(f16(f18(c50,X_1728),X_1729),X_1730)),c55),f13(f16(f18(c50,f20(f22(f24(f26(c56,X_1728),X_1729),X_1730),c54)),f30(f32(f34(f36(c57,X_1728),X_1729),X_1730),c54)),f40(f42(f44(f46(c58,X_1728),X_1729),X_1730),c54))) ),
inference(subst,[],[refute_0_23:[bind(X79,$fot(f13(f16(f18(c50,f20(f22(f24(f26(c56,X_1728),X_1729),X_1730),c54)),f30(f32(f34(f36(c57,X_1728),X_1729),X_1730),c54)),f40(f42(f44(f46(c58,X_1728),X_1729),X_1730),c54)))),bind(X_371,$fot(f10(c49,f13(f16(f18(c50,X_1728),X_1729),X_1730))))]]) ).
cnf(refute_0_25,plain,
p3(f8(f10(c49,f13(f16(f18(c50,X_1728),X_1729),X_1730)),c54),f13(f16(f18(c50,f20(f22(f24(f26(c56,X_1728),X_1729),X_1730),c54)),f30(f32(f34(f36(c57,X_1728),X_1729),X_1730),c54)),f40(f42(f44(f46(c58,X_1728),X_1729),X_1730),c54))),
inference(subst,[],[p3_80:[bind(X65,$fot(X_1728)),bind(X66,$fot(X_1729)),bind(X67,$fot(X_1730)),bind(X68,$fot(c54))]]) ).
cnf(refute_0_26,plain,
p3(f8(f10(c49,f13(f16(f18(c50,X_1728),X_1729),X_1730)),c55),f13(f16(f18(c50,f20(f22(f24(f26(c56,X_1728),X_1729),X_1730),c54)),f30(f32(f34(f36(c57,X_1728),X_1729),X_1730),c54)),f40(f42(f44(f46(c58,X_1728),X_1729),X_1730),c54))),
inference(resolve,[$cnf( p3(f8(f10(c49,f13(f16(f18(c50,X_1728),X_1729),X_1730)),c54),f13(f16(f18(c50,f20(f22(f24(f26(c56,X_1728),X_1729),X_1730),c54)),f30(f32(f34(f36(c57,X_1728),X_1729),X_1730),c54)),f40(f42(f44(f46(c58,X_1728),X_1729),X_1730),c54))) )],[refute_0_25,refute_0_24]) ).
cnf(refute_0_27,plain,
p3(f8(f10(c49,f13(f16(f18(c50,X_2228),X_2229),X_2230)),c55),f13(f16(f18(c50,f20(f22(f24(f26(c56,X_2228),X_2229),X_2230),c54)),f30(f32(f34(f36(c57,X_2228),X_2229),X_2230),c54)),f40(f42(f44(f46(c58,X_2228),X_2229),X_2230),c54))),
inference(subst,[],[refute_0_26:[bind(X_1728,$fot(X_2228)),bind(X_1729,$fot(X_2229)),bind(X_1730,$fot(X_2230))]]) ).
cnf(refute_0_28,plain,
p4(f5(X_219,f8(f10(c49,f13(f16(f18(c50,X_2228),X_2229),X_2230)),c55)),f5(X_219,f13(f16(f18(c50,f20(f22(f24(f26(c56,X_2228),X_2229),X_2230),c54)),f30(f32(f34(f36(c57,X_2228),X_2229),X_2230),c54)),f40(f42(f44(f46(c58,X_2228),X_2229),X_2230),c54)))),
inference(resolve,[$cnf( p3(f8(f10(c49,f13(f16(f18(c50,X_2228),X_2229),X_2230)),c55),f13(f16(f18(c50,f20(f22(f24(f26(c56,X_2228),X_2229),X_2230),c54)),f30(f32(f34(f36(c57,X_2228),X_2229),X_2230),c54)),f40(f42(f44(f46(c58,X_2228),X_2229),X_2230),c54))) )],[refute_0_27,refute_0_15]) ).
cnf(refute_0_29,plain,
p4(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c55)),f5(c48,f13(f16(f18(c50,f20(f22(f24(f26(c56,c51),c52),c53),c54)),f30(f32(f34(f36(c57,c51),c52),c53),c54)),f40(f42(f44(f46(c58,c51),c52),c53),c54)))),
inference(subst,[],[refute_0_28:[bind(X_219,$fot(c48)),bind(X_2228,$fot(c51)),bind(X_2229,$fot(c52)),bind(X_2230,$fot(c53))]]) ).
cnf(refute_0_30,plain,
( ~ p47(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54)),c55)
| p47(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54)),c54) ),
inference(subst,[],[refute_0_9:[bind(X_2510,$fot(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54))))]]) ).
cnf(refute_0_31,plain,
p47(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54)),c54),
inference(resolve,[$cnf( p47(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54)),c55) )],[p47_77,refute_0_30]) ).
cnf(refute_0_32,plain,
( ~ p3(f8(X_371,c54),f8(X_371,c55))
| p4(f5(X_219,f8(X_371,c54)),f5(X_219,f8(X_371,c55))) ),
inference(subst,[],[refute_0_14:[bind(X_218,$fot(f8(X_371,c54))),bind(X_220,$fot(f8(X_371,c55)))]]) ).
cnf(refute_0_33,plain,
p4(f5(X_219,f8(X_371,c54)),f5(X_219,f8(X_371,c55))),
inference(resolve,[$cnf( p3(f8(X_371,c54),f8(X_371,c55)) )],[refute_0_22,refute_0_32]) ).
cnf(refute_0_34,plain,
( ~ p4(X_2497,X_2495)
| ~ p47(X_2497,c54)
| ~ p7(c54,c55)
| p47(X_2495,c55) ),
inference(subst,[],[p47_53:[bind(X151,$fot(X_2495)),bind(X152,$fot(c55)),bind(X153,$fot(X_2497)),bind(X154,$fot(c54))]]) ).
cnf(refute_0_35,plain,
( ~ p4(X_2497,X_2495)
| ~ p47(X_2497,c54)
| p47(X_2495,c55) ),
inference(resolve,[$cnf( p7(c54,c55) )],[p7_26,refute_0_34]) ).
cnf(refute_0_36,plain,
( ~ p4(f5(X_219,f8(X_371,c54)),f5(X_219,f8(X_371,c55)))
| ~ p47(f5(X_219,f8(X_371,c54)),c54)
| p47(f5(X_219,f8(X_371,c55)),c55) ),
inference(subst,[],[refute_0_35:[bind(X_2495,$fot(f5(X_219,f8(X_371,c55)))),bind(X_2497,$fot(f5(X_219,f8(X_371,c54))))]]) ).
cnf(refute_0_37,plain,
( ~ p47(f5(X_219,f8(X_371,c54)),c54)
| p47(f5(X_219,f8(X_371,c55)),c55) ),
inference(resolve,[$cnf( p4(f5(X_219,f8(X_371,c54)),f5(X_219,f8(X_371,c55))) )],[refute_0_33,refute_0_36]) ).
cnf(refute_0_38,plain,
( ~ p47(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54)),c54)
| p47(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c55)),c55) ),
inference(subst,[],[refute_0_37:[bind(X_219,$fot(c48)),bind(X_371,$fot(f10(c49,f13(f16(f18(c50,c51),c52),c53))))]]) ).
cnf(refute_0_39,plain,
p47(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c55)),c55),
inference(resolve,[$cnf( p47(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54)),c54) )],[refute_0_31,refute_0_38]) ).
cnf(refute_0_40,plain,
p7(X_2496,X_2496),
inference(subst,[],[p7_3:[bind(X162,$fot(X_2496))]]) ).
cnf(refute_0_41,plain,
( ~ p4(X_2497,X_2495)
| ~ p47(X_2497,X_2496)
| ~ p7(X_2496,X_2496)
| p47(X_2495,X_2496) ),
inference(subst,[],[p47_53:[bind(X151,$fot(X_2495)),bind(X152,$fot(X_2496)),bind(X153,$fot(X_2497)),bind(X154,$fot(X_2496))]]) ).
cnf(refute_0_42,plain,
( ~ p4(X_2497,X_2495)
| ~ p47(X_2497,X_2496)
| p47(X_2495,X_2496) ),
inference(resolve,[$cnf( p7(X_2496,X_2496) )],[refute_0_40,refute_0_41]) ).
cnf(refute_0_43,plain,
( ~ p4(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c55)),X_2528)
| ~ p47(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c55)),c55)
| p47(X_2528,c55) ),
inference(subst,[],[refute_0_42:[bind(X_2495,$fot(X_2528)),bind(X_2496,$fot(c55)),bind(X_2497,$fot(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c55))))]]) ).
cnf(refute_0_44,plain,
( ~ p4(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c55)),X_2528)
| p47(X_2528,c55) ),
inference(resolve,[$cnf( p47(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c55)),c55) )],[refute_0_39,refute_0_43]) ).
cnf(refute_0_45,plain,
( ~ p4(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c55)),f5(c48,f13(f16(f18(c50,f20(f22(f24(f26(c56,c51),c52),c53),c54)),f30(f32(f34(f36(c57,c51),c52),c53),c54)),f40(f42(f44(f46(c58,c51),c52),c53),c54))))
| p47(f5(c48,f13(f16(f18(c50,f20(f22(f24(f26(c56,c51),c52),c53),c54)),f30(f32(f34(f36(c57,c51),c52),c53),c54)),f40(f42(f44(f46(c58,c51),c52),c53),c54))),c55) ),
inference(subst,[],[refute_0_44:[bind(X_2528,$fot(f5(c48,f13(f16(f18(c50,f20(f22(f24(f26(c56,c51),c52),c53),c54)),f30(f32(f34(f36(c57,c51),c52),c53),c54)),f40(f42(f44(f46(c58,c51),c52),c53),c54)))))]]) ).
cnf(refute_0_46,plain,
p47(f5(c48,f13(f16(f18(c50,f20(f22(f24(f26(c56,c51),c52),c53),c54)),f30(f32(f34(f36(c57,c51),c52),c53),c54)),f40(f42(f44(f46(c58,c51),c52),c53),c54))),c55),
inference(resolve,[$cnf( p4(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c55)),f5(c48,f13(f16(f18(c50,f20(f22(f24(f26(c56,c51),c52),c53),c54)),f30(f32(f34(f36(c57,c51),c52),c53),c54)),f40(f42(f44(f46(c58,c51),c52),c53),c54)))) )],[refute_0_29,refute_0_45]) ).
cnf(refute_0_47,plain,
p47(f20(f22(f24(f26(c56,c51),c52),c53),c54),c55),
inference(resolve,[$cnf( p47(f5(c48,f13(f16(f18(c50,f20(f22(f24(f26(c56,c51),c52),c53),c54)),f30(f32(f34(f36(c57,c51),c52),c53),c54)),f40(f42(f44(f46(c58,c51),c52),c53),c54))),c55) )],[refute_0_46,refute_0_11]) ).
cnf(refute_0_48,plain,
p47(f20(f22(f24(f26(c56,c51),c52),c53),c54),c54),
inference(resolve,[$cnf( p47(f20(f22(f24(f26(c56,c51),c52),c53),c54),c55) )],[refute_0_47,refute_0_10]) ).
cnf(refute_0_49,plain,
~ p47(f20(f22(f24(f26(c56,c51),c52),c53),c54),c54),
inference(subst,[],[not_p47_52:[bind(X65,$fot(c51)),bind(X66,$fot(c52)),bind(X67,$fot(c53)),bind(X68,$fot(c54))]]) ).
cnf(refute_0_50,plain,
$false,
inference(resolve,[$cnf( p47(f20(f22(f24(f26(c56,c51),c52),c53),c54),c54) )],[refute_0_48,refute_0_49]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SYN704-1 : TPTP v8.1.0. Released v2.5.0.
% 0.12/0.14 % Command : metis --show proof --show saturation %s
% 0.14/0.35 % Computer : n029.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 600
% 0.14/0.35 % DateTime : Mon Jul 11 15:04:17 EDT 2022
% 0.14/0.35 % CPUTime :
% 0.14/0.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.91/1.12 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.91/1.12
% 0.91/1.12 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 0.91/1.13
%------------------------------------------------------------------------------