%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SYN691-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n028.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:49 EDT 2022
% Result : Unsatisfiable 0.18s 0.45s
% Output : CNFRefutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 14
% Syntax : Number of clauses : 46 ( 22 unt; 0 nHn; 27 RR)
% Number of literals : 82 ( 0 equ; 37 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 10 con; 0-2 aty)
% Number of variables : 100 ( 10 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(p4_5,negated_conjecture,
p4(X111,X111) ).
cnf(p3_10,negated_conjecture,
p3(X68,X68) ).
cnf(p22_15,negated_conjecture,
p22(X37,X37) ).
cnf(p2_17,negated_conjecture,
p2(X31,X31) ).
cnf(p4_26,negated_conjecture,
( p4(X112,X113)
| ~ p4(X111,X112)
| ~ p4(X111,X113) ) ).
cnf(p3_31,negated_conjecture,
( p3(X69,X70)
| ~ p3(X68,X69)
| ~ p3(X68,X70) ) ).
cnf(not_p39_43,negated_conjecture,
~ p39(f5(c40,f10(f13(f15(c42,c43),c44),c45)),c46) ).
cnf(p39_44,negated_conjecture,
( p39(X47,X50)
| ~ p39(f17(f19(f21(c47,X47),X48),X49),X50) ) ).
cnf(p39_45,negated_conjecture,
( p39(X107,X108)
| ~ p39(X110,X109)
| ~ p4(X110,X107)
| ~ p22(X109,X108) ) ).
cnf(p39_46,negated_conjecture,
p39(f5(c40,f7(c41,f10(f13(f15(c42,c43),c44),c45))),c46) ).
cnf(p4_50,negated_conjecture,
( p4(f5(X118,X119),f5(X120,X121))
| ~ p2(X118,X120)
| ~ p3(X119,X121) ) ).
cnf(p39_63,negated_conjecture,
( p39(X103,X104)
| ~ p39(f5(c40,f10(f13(f15(c42,X103),X105),X106)),X104) ) ).
cnf(p39_64,negated_conjecture,
( p39(f5(c40,f10(f13(f15(c42,X103),X105),X106)),X104)
| ~ p39(X103,X104) ) ).
cnf(p3_67,negated_conjecture,
p3(f7(c41,f10(f13(f15(c42,X47),X48),X49)),f10(f13(f15(c42,f17(f19(f21(c47,X47),X48),X49)),f26(f28(f30(c48,X47),X48),X49)),f34(f36(f38(c49,X47),X48),X49))) ).
cnf(refute_0_0,plain,
( ~ p39(c43,c46)
| p39(f5(c40,f10(f13(f15(c42,c43),X105),X106)),c46) ),
inference(subst,[],[p39_64:[bind(X103,$fot(c43)),bind(X104,$fot(c46))]]) ).
cnf(refute_0_1,plain,
( ~ p39(f17(f19(f21(c47,c43),c44),c45),c46)
| p39(c43,c46) ),
inference(subst,[],[p39_44:[bind(X47,$fot(c43)),bind(X48,$fot(c44)),bind(X49,$fot(c45)),bind(X50,$fot(c46))]]) ).
cnf(refute_0_2,plain,
( ~ p39(f5(c40,f10(f13(f15(c42,f17(f19(f21(c47,c43),c44),c45)),f26(f28(f30(c48,c43),c44),c45)),f34(f36(f38(c49,c43),c44),c45))),c46)
| p39(f17(f19(f21(c47,c43),c44),c45),c46) ),
inference(subst,[],[p39_63:[bind(X103,$fot(f17(f19(f21(c47,c43),c44),c45))),bind(X104,$fot(c46)),bind(X105,$fot(f26(f28(f30(c48,c43),c44),c45))),bind(X106,$fot(f34(f36(f38(c49,c43),c44),c45)))]]) ).
cnf(refute_0_3,plain,
p4(X_43,X_43),
inference(subst,[],[p4_5:[bind(X111,$fot(X_43))]]) ).
cnf(refute_0_4,plain,
( ~ p4(X_43,X_42)
| ~ p4(X_43,X_43)
| p4(X_42,X_43) ),
inference(subst,[],[p4_26:[bind(X111,$fot(X_43)),bind(X112,$fot(X_42)),bind(X113,$fot(X_43))]]) ).
cnf(refute_0_5,plain,
( ~ p4(X_43,X_42)
| p4(X_42,X_43) ),
inference(resolve,[$cnf( p4(X_43,X_43) )],[refute_0_3,refute_0_4]) ).
cnf(refute_0_6,plain,
( ~ p4(f5(X_193,f10(f13(f15(c42,f17(f19(f21(c47,X_190),X_191),X_192)),f26(f28(f30(c48,X_190),X_191),X_192)),f34(f36(f38(c49,X_190),X_191),X_192))),f5(X_193,f7(c41,f10(f13(f15(c42,X_190),X_191),X_192))))
| p4(f5(X_193,f7(c41,f10(f13(f15(c42,X_190),X_191),X_192))),f5(X_193,f10(f13(f15(c42,f17(f19(f21(c47,X_190),X_191),X_192)),f26(f28(f30(c48,X_190),X_191),X_192)),f34(f36(f38(c49,X_190),X_191),X_192)))) ),
inference(subst,[],[refute_0_5:[bind(X_42,$fot(f5(X_193,f7(c41,f10(f13(f15(c42,X_190),X_191),X_192))))),bind(X_43,$fot(f5(X_193,f10(f13(f15(c42,f17(f19(f21(c47,X_190),X_191),X_192)),f26(f28(f30(c48,X_190),X_191),X_192)),f34(f36(f38(c49,X_190),X_191),X_192)))))]]) ).
cnf(refute_0_7,plain,
p3(X_68,X_68),
inference(subst,[],[p3_10:[bind(X68,$fot(X_68))]]) ).
cnf(refute_0_8,plain,
( ~ p3(X_68,X_67)
| ~ p3(X_68,X_68)
| p3(X_67,X_68) ),
inference(subst,[],[p3_31:[bind(X68,$fot(X_68)),bind(X69,$fot(X_67)),bind(X70,$fot(X_68))]]) ).
cnf(refute_0_9,plain,
( ~ p3(X_68,X_67)
| p3(X_67,X_68) ),
inference(resolve,[$cnf( p3(X_68,X_68) )],[refute_0_7,refute_0_8]) ).
cnf(refute_0_10,plain,
( ~ p3(f7(c41,f10(f13(f15(c42,X_140),X_141),X_142)),f10(f13(f15(c42,f17(f19(f21(c47,X_140),X_141),X_142)),f26(f28(f30(c48,X_140),X_141),X_142)),f34(f36(f38(c49,X_140),X_141),X_142)))
| p3(f10(f13(f15(c42,f17(f19(f21(c47,X_140),X_141),X_142)),f26(f28(f30(c48,X_140),X_141),X_142)),f34(f36(f38(c49,X_140),X_141),X_142)),f7(c41,f10(f13(f15(c42,X_140),X_141),X_142))) ),
inference(subst,[],[refute_0_9:[bind(X_67,$fot(f10(f13(f15(c42,f17(f19(f21(c47,X_140),X_141),X_142)),f26(f28(f30(c48,X_140),X_141),X_142)),f34(f36(f38(c49,X_140),X_141),X_142)))),bind(X_68,$fot(f7(c41,f10(f13(f15(c42,X_140),X_141),X_142))))]]) ).
cnf(refute_0_11,plain,
p3(f7(c41,f10(f13(f15(c42,X_140),X_141),X_142)),f10(f13(f15(c42,f17(f19(f21(c47,X_140),X_141),X_142)),f26(f28(f30(c48,X_140),X_141),X_142)),f34(f36(f38(c49,X_140),X_141),X_142))),
inference(subst,[],[p3_67:[bind(X47,$fot(X_140)),bind(X48,$fot(X_141)),bind(X49,$fot(X_142))]]) ).
cnf(refute_0_12,plain,
p3(f10(f13(f15(c42,f17(f19(f21(c47,X_140),X_141),X_142)),f26(f28(f30(c48,X_140),X_141),X_142)),f34(f36(f38(c49,X_140),X_141),X_142)),f7(c41,f10(f13(f15(c42,X_140),X_141),X_142))),
inference(resolve,[$cnf( p3(f7(c41,f10(f13(f15(c42,X_140),X_141),X_142)),f10(f13(f15(c42,f17(f19(f21(c47,X_140),X_141),X_142)),f26(f28(f30(c48,X_140),X_141),X_142)),f34(f36(f38(c49,X_140),X_141),X_142))) )],[refute_0_11,refute_0_10]) ).
cnf(refute_0_13,plain,
p2(X_182,X_182),
inference(subst,[],[p2_17:[bind(X31,$fot(X_182))]]) ).
cnf(refute_0_14,plain,
( ~ p2(X_182,X_182)
| ~ p3(X_181,X_183)
| p4(f5(X_182,X_181),f5(X_182,X_183)) ),
inference(subst,[],[p4_50:[bind(X118,$fot(X_182)),bind(X119,$fot(X_181)),bind(X120,$fot(X_182)),bind(X121,$fot(X_183))]]) ).
cnf(refute_0_15,plain,
( ~ p3(X_181,X_183)
| p4(f5(X_182,X_181),f5(X_182,X_183)) ),
inference(resolve,[$cnf( p2(X_182,X_182) )],[refute_0_13,refute_0_14]) ).
cnf(refute_0_16,plain,
( ~ p3(f10(f13(f15(c42,f17(f19(f21(c47,X_140),X_141),X_142)),f26(f28(f30(c48,X_140),X_141),X_142)),f34(f36(f38(c49,X_140),X_141),X_142)),f7(c41,f10(f13(f15(c42,X_140),X_141),X_142)))
| p4(f5(X_188,f10(f13(f15(c42,f17(f19(f21(c47,X_140),X_141),X_142)),f26(f28(f30(c48,X_140),X_141),X_142)),f34(f36(f38(c49,X_140),X_141),X_142))),f5(X_188,f7(c41,f10(f13(f15(c42,X_140),X_141),X_142)))) ),
inference(subst,[],[refute_0_15:[bind(X_181,$fot(f10(f13(f15(c42,f17(f19(f21(c47,X_140),X_141),X_142)),f26(f28(f30(c48,X_140),X_141),X_142)),f34(f36(f38(c49,X_140),X_141),X_142)))),bind(X_182,$fot(X_188)),bind(X_183,$fot(f7(c41,f10(f13(f15(c42,X_140),X_141),X_142))))]]) ).
cnf(refute_0_17,plain,
p4(f5(X_188,f10(f13(f15(c42,f17(f19(f21(c47,X_140),X_141),X_142)),f26(f28(f30(c48,X_140),X_141),X_142)),f34(f36(f38(c49,X_140),X_141),X_142))),f5(X_188,f7(c41,f10(f13(f15(c42,X_140),X_141),X_142)))),
inference(resolve,[$cnf( p3(f10(f13(f15(c42,f17(f19(f21(c47,X_140),X_141),X_142)),f26(f28(f30(c48,X_140),X_141),X_142)),f34(f36(f38(c49,X_140),X_141),X_142)),f7(c41,f10(f13(f15(c42,X_140),X_141),X_142))) )],[refute_0_12,refute_0_16]) ).
cnf(refute_0_18,plain,
p4(f5(X_193,f10(f13(f15(c42,f17(f19(f21(c47,X_190),X_191),X_192)),f26(f28(f30(c48,X_190),X_191),X_192)),f34(f36(f38(c49,X_190),X_191),X_192))),f5(X_193,f7(c41,f10(f13(f15(c42,X_190),X_191),X_192)))),
inference(subst,[],[refute_0_17:[bind(X_140,$fot(X_190)),bind(X_141,$fot(X_191)),bind(X_142,$fot(X_192)),bind(X_188,$fot(X_193))]]) ).
cnf(refute_0_19,plain,
p4(f5(X_193,f7(c41,f10(f13(f15(c42,X_190),X_191),X_192))),f5(X_193,f10(f13(f15(c42,f17(f19(f21(c47,X_190),X_191),X_192)),f26(f28(f30(c48,X_190),X_191),X_192)),f34(f36(f38(c49,X_190),X_191),X_192)))),
inference(resolve,[$cnf( p4(f5(X_193,f10(f13(f15(c42,f17(f19(f21(c47,X_190),X_191),X_192)),f26(f28(f30(c48,X_190),X_191),X_192)),f34(f36(f38(c49,X_190),X_191),X_192))),f5(X_193,f7(c41,f10(f13(f15(c42,X_190),X_191),X_192)))) )],[refute_0_18,refute_0_6]) ).
cnf(refute_0_20,plain,
p22(X_327,X_327),
inference(subst,[],[p22_15:[bind(X37,$fot(X_327))]]) ).
cnf(refute_0_21,plain,
( ~ p22(X_327,X_327)
| ~ p39(X_329,X_327)
| ~ p4(X_329,X_326)
| p39(X_326,X_327) ),
inference(subst,[],[p39_45:[bind(X107,$fot(X_326)),bind(X108,$fot(X_327)),bind(X109,$fot(X_327)),bind(X110,$fot(X_329))]]) ).
cnf(refute_0_22,plain,
( ~ p39(X_329,X_327)
| ~ p4(X_329,X_326)
| p39(X_326,X_327) ),
inference(resolve,[$cnf( p22(X_327,X_327) )],[refute_0_20,refute_0_21]) ).
cnf(refute_0_23,plain,
( ~ p39(f5(X_193,f7(c41,f10(f13(f15(c42,X_190),X_191),X_192))),X_331)
| ~ p4(f5(X_193,f7(c41,f10(f13(f15(c42,X_190),X_191),X_192))),f5(X_193,f10(f13(f15(c42,f17(f19(f21(c47,X_190),X_191),X_192)),f26(f28(f30(c48,X_190),X_191),X_192)),f34(f36(f38(c49,X_190),X_191),X_192))))
| p39(f5(X_193,f10(f13(f15(c42,f17(f19(f21(c47,X_190),X_191),X_192)),f26(f28(f30(c48,X_190),X_191),X_192)),f34(f36(f38(c49,X_190),X_191),X_192))),X_331) ),
inference(subst,[],[refute_0_22:[bind(X_326,$fot(f5(X_193,f10(f13(f15(c42,f17(f19(f21(c47,X_190),X_191),X_192)),f26(f28(f30(c48,X_190),X_191),X_192)),f34(f36(f38(c49,X_190),X_191),X_192))))),bind(X_327,$fot(X_331)),bind(X_329,$fot(f5(X_193,f7(c41,f10(f13(f15(c42,X_190),X_191),X_192)))))]]) ).
cnf(refute_0_24,plain,
( ~ p39(f5(X_193,f7(c41,f10(f13(f15(c42,X_190),X_191),X_192))),X_331)
| p39(f5(X_193,f10(f13(f15(c42,f17(f19(f21(c47,X_190),X_191),X_192)),f26(f28(f30(c48,X_190),X_191),X_192)),f34(f36(f38(c49,X_190),X_191),X_192))),X_331) ),
inference(resolve,[$cnf( p4(f5(X_193,f7(c41,f10(f13(f15(c42,X_190),X_191),X_192))),f5(X_193,f10(f13(f15(c42,f17(f19(f21(c47,X_190),X_191),X_192)),f26(f28(f30(c48,X_190),X_191),X_192)),f34(f36(f38(c49,X_190),X_191),X_192)))) )],[refute_0_19,refute_0_23]) ).
cnf(refute_0_25,plain,
( ~ p39(f5(c40,f7(c41,f10(f13(f15(c42,c43),c44),c45))),c46)
| p39(f5(c40,f10(f13(f15(c42,f17(f19(f21(c47,c43),c44),c45)),f26(f28(f30(c48,c43),c44),c45)),f34(f36(f38(c49,c43),c44),c45))),c46) ),
inference(subst,[],[refute_0_24:[bind(X_190,$fot(c43)),bind(X_191,$fot(c44)),bind(X_192,$fot(c45)),bind(X_193,$fot(c40)),bind(X_331,$fot(c46))]]) ).
cnf(refute_0_26,plain,
p39(f5(c40,f10(f13(f15(c42,f17(f19(f21(c47,c43),c44),c45)),f26(f28(f30(c48,c43),c44),c45)),f34(f36(f38(c49,c43),c44),c45))),c46),
inference(resolve,[$cnf( p39(f5(c40,f7(c41,f10(f13(f15(c42,c43),c44),c45))),c46) )],[p39_46,refute_0_25]) ).
cnf(refute_0_27,plain,
p39(f17(f19(f21(c47,c43),c44),c45),c46),
inference(resolve,[$cnf( p39(f5(c40,f10(f13(f15(c42,f17(f19(f21(c47,c43),c44),c45)),f26(f28(f30(c48,c43),c44),c45)),f34(f36(f38(c49,c43),c44),c45))),c46) )],[refute_0_26,refute_0_2]) ).
cnf(refute_0_28,plain,
p39(c43,c46),
inference(resolve,[$cnf( p39(f17(f19(f21(c47,c43),c44),c45),c46) )],[refute_0_27,refute_0_1]) ).
cnf(refute_0_29,plain,
p39(f5(c40,f10(f13(f15(c42,c43),X105),X106)),c46),
inference(resolve,[$cnf( p39(c43,c46) )],[refute_0_28,refute_0_0]) ).
cnf(refute_0_30,plain,
p39(f5(c40,f10(f13(f15(c42,c43),c44),c45)),c46),
inference(subst,[],[refute_0_29:[bind(X105,$fot(c44)),bind(X106,$fot(c45))]]) ).
cnf(refute_0_31,plain,
$false,
inference(resolve,[$cnf( p39(f5(c40,f10(f13(f15(c42,c43),c44),c45)),c46) )],[refute_0_30,not_p39_43]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : SYN691-1 : TPTP v8.1.0. Released v2.5.0.
% 0.06/0.11 % Command : metis --show proof --show saturation %s
% 0.11/0.32 % Computer : n028.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 600
% 0.11/0.32 % DateTime : Mon Jul 11 13:31:13 EDT 2022
% 0.11/0.32 % CPUTime :
% 0.11/0.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.18/0.45 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.45
% 0.18/0.45 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 0.18/0.46
%------------------------------------------------------------------------------