%------------------------------------------------------------------------------
% File : Otter---3.3
% Problem : SYN691-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : otter-tptp-script %s
% Computer : n009.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 : 300s
% DateTime : Wed Jul 27 13:25:07 EDT 2022
% Result : Unsatisfiable 1.78s 1.98s
% Output : Refutation 1.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 10
% Syntax : Number of clauses : 16 ( 11 unt; 0 nHn; 10 RR)
% Number of literals : 24 ( 0 equ; 9 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 : 31 ( 8 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(22,axiom,
~ p39(f5(c40,f10(f13(f15(c42,c43),c44),c45)),c46),
file('SYN691-1.p',unknown),
[] ).
cnf(23,axiom,
( p39(A,B)
| ~ p39(f17(f19(f21(c47,A),C),D),B) ),
file('SYN691-1.p',unknown),
[] ).
cnf(24,axiom,
( p39(A,B)
| ~ p39(C,D)
| ~ p4(C,A)
| ~ p22(D,B) ),
file('SYN691-1.p',unknown),
[] ).
cnf(28,axiom,
( p4(f5(A,B),f5(C,D))
| ~ p2(A,C)
| ~ p3(B,D) ),
file('SYN691-1.p',unknown),
[] ).
cnf(41,axiom,
( p39(A,B)
| ~ p39(f5(c40,f10(f13(f15(c42,A),C),D)),B) ),
file('SYN691-1.p',unknown),
[] ).
cnf(42,axiom,
( p39(f5(c40,f10(f13(f15(c42,A),B),C)),D)
| ~ p39(A,D) ),
file('SYN691-1.p',unknown),
[] ).
cnf(59,axiom,
p22(A,A),
file('SYN691-1.p',unknown),
[] ).
cnf(61,axiom,
p2(A,A),
file('SYN691-1.p',unknown),
[] ).
cnf(66,axiom,
p39(f5(c40,f7(c41,f10(f13(f15(c42,c43),c44),c45))),c46),
file('SYN691-1.p',unknown),
[] ).
cnf(67,axiom,
p3(f7(c41,f10(f13(f15(c42,A),B),C)),f10(f13(f15(c42,f17(f19(f21(c47,A),B),C)),f26(f28(f30(c48,A),B),C)),f34(f36(f38(c49,A),B),C))),
file('SYN691-1.p',unknown),
[] ).
cnf(72,plain,
p4(f5(A,f7(c41,f10(f13(f15(c42,B),C),D))),f5(A,f10(f13(f15(c42,f17(f19(f21(c47,B),C),D)),f26(f28(f30(c48,B),C),D)),f34(f36(f38(c49,B),C),D)))),
inference(hyper,[status(thm)],[67,28,61]),
[iquote('hyper,67,28,61')] ).
cnf(83,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(hyper,[status(thm)],[72,24,66,59]),
[iquote('hyper,72,24,66,59')] ).
cnf(85,plain,
p39(f17(f19(f21(c47,c43),c44),c45),c46),
inference(hyper,[status(thm)],[83,41]),
[iquote('hyper,83,41')] ).
cnf(90,plain,
p39(c43,c46),
inference(hyper,[status(thm)],[85,23]),
[iquote('hyper,85,23')] ).
cnf(91,plain,
p39(f5(c40,f10(f13(f15(c42,c43),A),B)),c46),
inference(hyper,[status(thm)],[90,42]),
[iquote('hyper,90,42')] ).
cnf(92,plain,
$false,
inference(binary,[status(thm)],[91,22]),
[iquote('binary,91.1,22.1')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYN691-1 : TPTP v8.1.0. Released v2.5.0.
% 0.03/0.12 % Command : otter-tptp-script %s
% 0.12/0.33 % Computer : n009.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Jul 27 10:56:36 EDT 2022
% 0.12/0.33 % CPUTime :
% 1.78/1.97 ----- Otter 3.3f, August 2004 -----
% 1.78/1.97 The process was started by sandbox2 on n009.cluster.edu,
% 1.78/1.97 Wed Jul 27 10:56:36 2022
% 1.78/1.97 The command was "./otter". The process ID is 31395.
% 1.78/1.97
% 1.78/1.97 set(prolog_style_variables).
% 1.78/1.97 set(auto).
% 1.78/1.97 dependent: set(auto1).
% 1.78/1.97 dependent: set(process_input).
% 1.78/1.97 dependent: clear(print_kept).
% 1.78/1.97 dependent: clear(print_new_demod).
% 1.78/1.97 dependent: clear(print_back_demod).
% 1.78/1.97 dependent: clear(print_back_sub).
% 1.78/1.97 dependent: set(control_memory).
% 1.78/1.97 dependent: assign(max_mem, 12000).
% 1.78/1.97 dependent: assign(pick_given_ratio, 4).
% 1.78/1.97 dependent: assign(stats_level, 1).
% 1.78/1.97 dependent: assign(max_seconds, 10800).
% 1.78/1.97 clear(print_given).
% 1.78/1.97
% 1.78/1.97 list(usable).
% 1.78/1.97 0 [] p11(X0,X0).
% 1.78/1.97 0 [] p9(X132,X132).
% 1.78/1.97 0 [] p8(X125,X125).
% 1.78/1.97 0 [] p6(X122,X122).
% 1.78/1.97 0 [] p4(X111,X111).
% 1.78/1.97 0 [] p37(X100,X100).
% 1.78/1.97 0 [] p35(X93,X93).
% 1.78/1.97 0 [] p33(X86,X86).
% 1.78/1.97 0 [] p31(X79,X79).
% 1.78/1.97 0 [] p3(X68,X68).
% 1.78/1.97 0 [] p29(X65,X65).
% 1.78/1.97 0 [] p27(X58,X58).
% 1.78/1.97 0 [] p25(X51,X51).
% 1.78/1.97 0 [] p23(X40,X40).
% 1.78/1.97 0 [] p22(X37,X37).
% 1.78/1.97 0 [] p20(X34,X34).
% 1.78/1.97 0 [] p2(X31,X31).
% 1.78/1.97 0 [] p18(X24,X24).
% 1.78/1.97 0 [] p16(X17,X17).
% 1.78/1.97 0 [] p14(X14,X14).
% 1.78/1.97 0 [] p12(X7,X7).
% 1.78/1.97 0 [] p11(X1,X2)| -p11(X0,X1)| -p11(X0,X2).
% 1.78/1.97 0 [] p9(X133,X134)| -p9(X132,X133)| -p9(X132,X134).
% 1.78/1.97 0 [] p8(X126,X127)| -p8(X125,X126)| -p8(X125,X127).
% 1.78/1.97 0 [] p6(X123,X124)| -p6(X122,X123)| -p6(X122,X124).
% 1.78/1.97 0 [] p4(X112,X113)| -p4(X111,X112)| -p4(X111,X113).
% 1.78/1.97 0 [] p37(X101,X102)| -p37(X100,X101)| -p37(X100,X102).
% 1.78/1.97 0 [] p35(X94,X95)| -p35(X93,X94)| -p35(X93,X95).
% 1.78/1.97 0 [] p33(X87,X88)| -p33(X86,X87)| -p33(X86,X88).
% 1.78/1.97 0 [] p31(X80,X81)| -p31(X79,X80)| -p31(X79,X81).
% 1.78/1.97 0 [] p3(X69,X70)| -p3(X68,X69)| -p3(X68,X70).
% 1.78/1.97 0 [] p29(X66,X67)| -p29(X65,X66)| -p29(X65,X67).
% 1.78/1.97 0 [] p27(X59,X60)| -p27(X58,X59)| -p27(X58,X60).
% 1.78/1.97 0 [] p25(X52,X53)| -p25(X51,X52)| -p25(X51,X53).
% 1.78/1.97 0 [] p23(X41,X42)| -p23(X40,X41)| -p23(X40,X42).
% 1.78/1.97 0 [] p22(X38,X39)| -p22(X37,X38)| -p22(X37,X39).
% 1.78/1.97 0 [] p20(X35,X36)| -p20(X34,X35)| -p20(X34,X36).
% 1.78/1.97 0 [] p2(X32,X33)| -p2(X31,X32)| -p2(X31,X33).
% 1.78/1.97 0 [] p18(X25,X26)| -p18(X24,X26)| -p18(X24,X25).
% 1.78/1.97 0 [] p16(X18,X19)| -p16(X17,X18)| -p16(X17,X19).
% 1.78/1.97 0 [] p14(X15,X16)| -p14(X14,X15)| -p14(X14,X16).
% 1.78/1.97 0 [] p12(X8,X9)| -p12(X7,X8)| -p12(X7,X9).
% 1.78/1.97 0 [] -p39(f5(c40,f10(f13(f15(c42,c43),c44),c45)),c46).
% 1.78/1.97 0 [] p39(X47,X50)| -p39(f17(f19(f21(c47,X47),X48),X49),X50).
% 1.78/1.97 0 [] p39(X107,X108)| -p39(X110,X109)| -p4(X110,X107)| -p22(X109,X108).
% 1.78/1.97 0 [] p39(f5(c40,f7(c41,f10(f13(f15(c42,c43),c44),c45))),c46).
% 1.78/1.97 0 [] p11(f15(X3,X4),f15(X5,X6))| -p14(X3,X5)| -p4(X4,X6).
% 1.78/1.97 0 [] p9(f34(X135,X136),f34(X137,X138))| -p33(X135,X137)| -p9(X136,X138).
% 1.78/1.97 0 [] p8(f13(X128,X129),f13(X130,X131))| -p11(X128,X130)| -p12(X129,X131).
% 1.78/1.97 0 [] p4(f5(X118,X119),f5(X120,X121))| -p2(X118,X120)| -p3(X119,X121).
% 1.78/1.97 0 [] p4(f17(X114,X115),f17(X116,X117))| -p16(X114,X116)| -p9(X115,X117).
% 1.78/1.97 0 [] p35(f38(X96,X97),f38(X98,X99))| -p37(X96,X98)| -p4(X97,X99).
% 1.78/1.97 0 [] p33(f36(X89,X90),f36(X91,X92))| -p12(X90,X92)| -p35(X89,X91).
% 1.78/1.97 0 [] p31(f32(X82,X83),f32(X84,X85))| -p22(X83,X85)| -p9(X82,X84).
% 1.78/1.97 0 [] p3(f7(X75,X76),f7(X77,X78))| -p3(X76,X78)| -p6(X75,X77).
% 1.78/1.97 0 [] p3(f10(X71,X72),f10(X73,X74))| -p8(X71,X73)| -p9(X72,X74).
% 1.78/1.97 0 [] p27(f30(X61,X62),f30(X63,X64))| -p29(X61,X63)| -p4(X62,X64).
% 1.78/1.97 0 [] p25(f28(X54,X55),f28(X56,X57))| -p12(X55,X57)| -p27(X54,X56).
% 1.78/1.97 0 [] p23(f24(X43,X44),f24(X45,X46))| -p12(X43,X45)| -p22(X44,X46).
% 1.78/1.97 0 [] p18(f21(X27,X28),f21(X29,X30))| -p20(X27,X29)| -p4(X28,X30).
% 1.78/1.97 0 [] p16(f19(X20,X21),f19(X22,X23))| -p12(X21,X23)| -p18(X20,X22).
% 1.78/1.97 0 [] p12(f26(X10,X11),f26(X12,X13))| -p25(X10,X12)| -p9(X11,X13).
% 1.78/1.97 0 [] p39(X103,X104)| -p39(f5(c40,f10(f13(f15(c42,X103),X105),X106)),X104).
% 1.78/1.97 0 [] p39(f5(c40,f10(f13(f15(c42,X103),X105),X106)),X104)| -p39(X103,X104).
% 1.78/1.97 0 [] p23(f24(f26(f28(f30(c48,X47),X48),X49),X50),f24(X48,X50))| -p39(f17(f19(f21(c47,X47),X48),X49),X50).
% 1.78/1.97 0 [] p31(f32(f34(f36(f38(c49,X47),X48),X49),X50),f32(X49,X50))| -p39(f17(f19(f21(c47,X47),X48),X49),X50).
% 1.78/1.97 0 [] 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))).
% 1.78/1.97 end_of_list.
% 1.78/1.97
% 1.78/1.97 SCAN INPUT: prop=0, horn=1, equality=0, symmetry=0, max_lits=4.
% 1.78/1.97
% 1.78/1.97 This is a Horn set without equality. The strategy will
% 1.78/1.97 be hyperresolution, with satellites in sos and nuclei
% 1.78/1.97 in usable.
% 1.78/1.97
% 1.78/1.97 dependent: set(hyper_res).
% 1.78/1.97 dependent: clear(order_hyper).
% 1.78/1.97
% 1.78/1.97 ------------> process usable:
% 1.78/1.97 ** KEPT (pick-wt=9): 1 [] p11(A,B)| -p11(C,A)| -p11(C,B).
% 1.78/1.97 ** KEPT (pick-wt=9): 2 [] p9(A,B)| -p9(C,A)| -p9(C,B).
% 1.78/1.97 ** KEPT (pick-wt=9): 3 [] p8(A,B)| -p8(C,A)| -p8(C,B).
% 1.78/1.97 ** KEPT (pick-wt=9): 4 [] p6(A,B)| -p6(C,A)| -p6(C,B).
% 1.78/1.97 ** KEPT (pick-wt=9): 5 [] p4(A,B)| -p4(C,A)| -p4(C,B).
% 1.78/1.97 ** KEPT (pick-wt=9): 6 [] p37(A,B)| -p37(C,A)| -p37(C,B).
% 1.78/1.97 ** KEPT (pick-wt=9): 7 [] p35(A,B)| -p35(C,A)| -p35(C,B).
% 1.78/1.97 ** KEPT (pick-wt=9): 8 [] p33(A,B)| -p33(C,A)| -p33(C,B).
% 1.78/1.97 ** KEPT (pick-wt=9): 9 [] p31(A,B)| -p31(C,A)| -p31(C,B).
% 1.78/1.97 ** KEPT (pick-wt=9): 10 [] p3(A,B)| -p3(C,A)| -p3(C,B).
% 1.78/1.97 ** KEPT (pick-wt=9): 11 [] p29(A,B)| -p29(C,A)| -p29(C,B).
% 1.78/1.97 ** KEPT (pick-wt=9): 12 [] p27(A,B)| -p27(C,A)| -p27(C,B).
% 1.78/1.97 ** KEPT (pick-wt=9): 13 [] p25(A,B)| -p25(C,A)| -p25(C,B).
% 1.78/1.97 ** KEPT (pick-wt=9): 14 [] p23(A,B)| -p23(C,A)| -p23(C,B).
% 1.78/1.97 ** KEPT (pick-wt=9): 15 [] p22(A,B)| -p22(C,A)| -p22(C,B).
% 1.78/1.97 ** KEPT (pick-wt=9): 16 [] p20(A,B)| -p20(C,A)| -p20(C,B).
% 1.78/1.97 ** KEPT (pick-wt=9): 17 [] p2(A,B)| -p2(C,A)| -p2(C,B).
% 1.78/1.97 ** KEPT (pick-wt=9): 18 [] p18(A,B)| -p18(C,B)| -p18(C,A).
% 1.78/1.97 ** KEPT (pick-wt=9): 19 [] p16(A,B)| -p16(C,A)| -p16(C,B).
% 1.78/1.97 ** KEPT (pick-wt=9): 20 [] p14(A,B)| -p14(C,A)| -p14(C,B).
% 1.78/1.97 ** KEPT (pick-wt=9): 21 [] p12(A,B)| -p12(C,A)| -p12(C,B).
% 1.78/1.97 ** KEPT (pick-wt=11): 22 [] -p39(f5(c40,f10(f13(f15(c42,c43),c44),c45)),c46).
% 1.78/1.97 ** KEPT (pick-wt=12): 23 [] p39(A,B)| -p39(f17(f19(f21(c47,A),C),D),B).
% 1.78/1.97 ** KEPT (pick-wt=12): 24 [] p39(A,B)| -p39(C,D)| -p4(C,A)| -p22(D,B).
% 1.78/1.97 ** KEPT (pick-wt=13): 25 [] p11(f15(A,B),f15(C,D))| -p14(A,C)| -p4(B,D).
% 1.78/1.97 ** KEPT (pick-wt=13): 26 [] p9(f34(A,B),f34(C,D))| -p33(A,C)| -p9(B,D).
% 1.78/1.97 ** KEPT (pick-wt=13): 27 [] p8(f13(A,B),f13(C,D))| -p11(A,C)| -p12(B,D).
% 1.78/1.97 ** KEPT (pick-wt=13): 28 [] p4(f5(A,B),f5(C,D))| -p2(A,C)| -p3(B,D).
% 1.78/1.97 ** KEPT (pick-wt=13): 29 [] p4(f17(A,B),f17(C,D))| -p16(A,C)| -p9(B,D).
% 1.78/1.97 ** KEPT (pick-wt=13): 30 [] p35(f38(A,B),f38(C,D))| -p37(A,C)| -p4(B,D).
% 1.78/1.97 ** KEPT (pick-wt=13): 31 [] p33(f36(A,B),f36(C,D))| -p12(B,D)| -p35(A,C).
% 1.78/1.97 ** KEPT (pick-wt=13): 32 [] p31(f32(A,B),f32(C,D))| -p22(B,D)| -p9(A,C).
% 1.78/1.97 ** KEPT (pick-wt=13): 33 [] p3(f7(A,B),f7(C,D))| -p3(B,D)| -p6(A,C).
% 1.78/1.97 ** KEPT (pick-wt=13): 34 [] p3(f10(A,B),f10(C,D))| -p8(A,C)| -p9(B,D).
% 1.78/1.97 ** KEPT (pick-wt=13): 35 [] p27(f30(A,B),f30(C,D))| -p29(A,C)| -p4(B,D).
% 1.78/1.97 ** KEPT (pick-wt=13): 36 [] p25(f28(A,B),f28(C,D))| -p12(B,D)| -p27(A,C).
% 1.78/1.97 ** KEPT (pick-wt=13): 37 [] p23(f24(A,B),f24(C,D))| -p12(A,C)| -p22(B,D).
% 1.78/1.97 ** KEPT (pick-wt=13): 38 [] p18(f21(A,B),f21(C,D))| -p20(A,C)| -p4(B,D).
% 1.78/1.97 ** KEPT (pick-wt=13): 39 [] p16(f19(A,B),f19(C,D))| -p12(B,D)| -p18(A,C).
% 1.78/1.97 ** KEPT (pick-wt=13): 40 [] p12(f26(A,B),f26(C,D))| -p25(A,C)| -p9(B,D).
% 1.78/1.97 ** KEPT (pick-wt=14): 41 [] p39(A,B)| -p39(f5(c40,f10(f13(f15(c42,A),C),D)),B).
% 1.78/1.97 ** KEPT (pick-wt=14): 42 [] p39(f5(c40,f10(f13(f15(c42,A),B),C)),D)| -p39(A,D).
% 1.78/1.97 ** KEPT (pick-wt=22): 43 [] p23(f24(f26(f28(f30(c48,A),B),C),D),f24(B,D))| -p39(f17(f19(f21(c47,A),B),C),D).
% 1.78/1.97 ** KEPT (pick-wt=22): 44 [] p31(f32(f34(f36(f38(c49,A),B),C),D),f32(C,D))| -p39(f17(f19(f21(c47,A),B),C),D).
% 1.78/1.97
% 1.78/1.97 ------------> process sos:
% 1.78/1.97 ** KEPT (pick-wt=3): 45 [] p11(A,A).
% 1.78/1.97 ** KEPT (pick-wt=3): 46 [] p9(A,A).
% 1.78/1.97 ** KEPT (pick-wt=3): 47 [] p8(A,A).
% 1.78/1.97 ** KEPT (pick-wt=3): 48 [] p6(A,A).
% 1.78/1.97 ** KEPT (pick-wt=3): 49 [] p4(A,A).
% 1.78/1.97 ** KEPT (pick-wt=3): 50 [] p37(A,A).
% 1.78/1.97 ** KEPT (pick-wt=3): 51 [] p35(A,A).
% 1.78/1.97 ** KEPT (pick-wt=3): 52 [] p33(A,A).
% 1.78/1.97 ** KEPT (pick-wt=3): 53 [] p31(A,A).
% 1.78/1.97 ** KEPT (pick-wt=3): 54 [] p3(A,A).
% 1.78/1.97 ** KEPT (pick-wt=3): 55 [] p29(A,A).
% 1.78/1.97 ** KEPT (pick-wt=3): 56 [] p27(A,A).
% 1.78/1.97 ** KEPT (pick-wt=3): 57 [] p25(A,A).
% 1.78/1.97 ** KEPT (pick-wt=3): 58 [] p23(A,A).
% 1.78/1.97 ** KEPT (pick-wt=3): 59 [] p22(A,A).
% 1.78/1.97 ** KEPT (pick-wt=3): 60 [] p20(A,A).
% 1.78/1.97 ** KEPT (pick-wt=3): 61 [] p2(A,A).
% 1.78/1.97 ** KEPT (pick-wt=3): 62 [] p18(A,A).
% 1.78/1.97 ** KEPT (pick-wt=3): 63 [] p16(A,A).
% 1.78/1.97 ** KEPT (pick-wt=3): 64 [] p14(A,A).
% 1.78/1.97 ** KEPT (pick-wt=3): 65 [] p12(A,A).
% 1.78/1.97 ** KEPT (pick-wt=13): 66 [] p39(f5(c40,f7(c41,f10(f13(f15(c42,c43),c44),c45))),c46).
% 1.78/1.97 ** KEPT (pick-wt=35): 67 [] p3(f7(c41,f10(f13(f15(c42,A),B),C)),f10(f13(f15(c42,f17(f19(f21(c47,A),B),C)),f26(f28(f30(c48,A),B),C)),f34(f36(f38(c49,A),B),C))).
% 1.78/1.98
% 1.78/1.98 ======= end of input processing =======
% 1.78/1.98
% 1.78/1.98 =========== start of search ===========
% 1.78/1.98
% 1.78/1.98 -------- PROOF --------
% 1.78/1.98
% 1.78/1.98 ----> UNIT CONFLICT at 0.01 sec ----> 92 [binary,91.1,22.1] $F.
% 1.78/1.98
% 1.78/1.98 Length of proof is 5. Level of proof is 5.
% 1.78/1.98
% 1.78/1.98 ---------------- PROOF ----------------
% 1.78/1.98 % SZS status Unsatisfiable
% 1.78/1.98 % SZS output start Refutation
% See solution above
% 1.78/1.98 ------------ end of proof -------------
% 1.78/1.98
% 1.78/1.98
% 1.78/1.98 Search stopped by max_proofs option.
% 1.78/1.98
% 1.78/1.98
% 1.78/1.98 Search stopped by max_proofs option.
% 1.78/1.98
% 1.78/1.98 ============ end of search ============
% 1.78/1.98
% 1.78/1.98 -------------- statistics -------------
% 1.78/1.98 clauses given 33
% 1.78/1.98 clauses generated 108
% 1.78/1.98 clauses kept 91
% 1.78/1.98 clauses forward subsumed 84
% 1.78/1.98 clauses back subsumed 1
% 1.78/1.98 Kbytes malloced 2929
% 1.78/1.98
% 1.78/1.98 ----------- times (seconds) -----------
% 1.78/1.98 user CPU time 0.01 (0 hr, 0 min, 0 sec)
% 1.78/1.98 system CPU time 0.00 (0 hr, 0 min, 0 sec)
% 1.78/1.98 wall-clock time 1 (0 hr, 0 min, 1 sec)
% 1.78/1.98
% 1.78/1.98 That finishes the proof of the theorem.
% 1.78/1.98
% 1.78/1.98 Process 31395 finished Wed Jul 27 10:56:37 2022
% 1.78/1.98 Otter interrupted
% 1.78/1.98 PROOF FOUND
%------------------------------------------------------------------------------