%------------------------------------------------------------------------------
% File : Otter---3.3
% Problem : SYN714-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : otter-tptp-script %s
% Computer : n027.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:10 EDT 2022
% Result : Unsatisfiable 1.83s 2.04s
% Output : Refutation 1.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 2
% Number of leaves : 8
% Syntax : Number of clauses : 11 ( 8 unt; 1 nHn; 9 RR)
% Number of literals : 18 ( 0 equ; 8 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 8 con; 0-2 aty)
% Number of variables : 8 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
~ p16(f17(c66),c65),
file('SYN714-1.p',unknown),
[] ).
cnf(4,axiom,
~ p50(c66,f25(f27(c59,c68),c67),c60),
file('SYN714-1.p',unknown),
[] ).
cnf(35,axiom,
( p50(c66,f25(f27(c59,A),c67),c62)
| ~ p53(A,f17(c66)) ),
file('SYN714-1.p',unknown),
[] ).
cnf(58,axiom,
( p51(A,f25(f27(B,C),D))
| ~ p51(A,D)
| ~ p53(C,f17(A)) ),
file('SYN714-1.p',unknown),
[] ).
cnf(69,axiom,
( p16(f17(A),c65)
| p50(A,B,c60)
| ~ p51(A,B)
| ~ p50(A,B,c62)
| ~ p52(f20(f21(c62,c64)),A) ),
file('SYN714-1.p',unknown),
[] ).
cnf(124,axiom,
p51(c66,c67),
file('SYN714-1.p',unknown),
[] ).
cnf(125,axiom,
p53(c68,f17(c66)),
file('SYN714-1.p',unknown),
[] ).
cnf(129,axiom,
p52(f20(f21(c62,c64)),c66),
file('SYN714-1.p',unknown),
[] ).
cnf(132,plain,
p51(c66,f25(f27(A,c68),c67)),
inference(hyper,[status(thm)],[125,58,124]),
[iquote('hyper,125,58,124')] ).
cnf(133,plain,
p50(c66,f25(f27(c59,c68),c67),c62),
inference(hyper,[status(thm)],[125,35]),
[iquote('hyper,125,35')] ).
cnf(171,plain,
$false,
inference(unit_del,[status(thm)],[inference(hyper,[status(thm)],[133,69,132,129]),1,4]),
[iquote('hyper,133,69,132,129,unit_del,1,4')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SYN714-1 : TPTP v8.1.0. Released v2.5.0.
% 0.00/0.12 % Command : otter-tptp-script %s
% 0.12/0.33 % Computer : n027.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 11:28:36 EDT 2022
% 0.12/0.33 % CPUTime :
% 1.83/2.03 ----- Otter 3.3f, August 2004 -----
% 1.83/2.03 The process was started by sandbox2 on n027.cluster.edu,
% 1.83/2.03 Wed Jul 27 11:28:37 2022
% 1.83/2.03 The command was "./otter". The process ID is 15310.
% 1.83/2.03
% 1.83/2.03 set(prolog_style_variables).
% 1.83/2.03 set(auto).
% 1.83/2.03 dependent: set(auto1).
% 1.83/2.03 dependent: set(process_input).
% 1.83/2.03 dependent: clear(print_kept).
% 1.83/2.03 dependent: clear(print_new_demod).
% 1.83/2.03 dependent: clear(print_back_demod).
% 1.83/2.03 dependent: clear(print_back_sub).
% 1.83/2.03 dependent: set(control_memory).
% 1.83/2.03 dependent: assign(max_mem, 12000).
% 1.83/2.03 dependent: assign(pick_given_ratio, 4).
% 1.83/2.03 dependent: assign(stats_level, 1).
% 1.83/2.03 dependent: assign(max_seconds, 10800).
% 1.83/2.03 clear(print_given).
% 1.83/2.03
% 1.83/2.03 list(usable).
% 1.83/2.03 0 [] p48(c62).
% 1.83/2.03 0 [] p47(c60).
% 1.83/2.03 0 [] p10(X0,X0).
% 1.83/2.03 0 [] p7(X201,X201).
% 1.83/2.03 0 [] p5(X141,X141).
% 1.83/2.03 0 [] p42(X120,X120).
% 1.83/2.03 0 [] p40(X115,X115).
% 1.83/2.03 0 [] p36(X112,X112).
% 1.83/2.03 0 [] p33(X105,X105).
% 1.83/2.03 0 [] p32(X98,X98).
% 1.83/2.03 0 [] p30(X95,X95).
% 1.83/2.03 0 [] p3(X80,X80).
% 1.83/2.03 0 [] p28(X73,X73).
% 1.83/2.03 0 [] p26(X64,X64).
% 1.83/2.03 0 [] p24(X55,X55).
% 1.83/2.03 0 [] p23(X48,X48).
% 1.83/2.03 0 [] p2(X35,X35).
% 1.83/2.03 0 [] p19(X30,X30).
% 1.83/2.03 0 [] p18(X23,X23).
% 1.83/2.03 0 [] p16(X12,X12).
% 1.83/2.03 0 [] p15(X7,X7).
% 1.83/2.03 0 [] p51(c66,c67).
% 1.83/2.03 0 [] p53(c68,f17(c66)).
% 1.83/2.03 0 [] -p16(f17(c66),c65).
% 1.83/2.03 0 [] p10(f11(c62),f11(c60)).
% 1.83/2.03 0 [] p49(f4(c60),f4(c62)).
% 1.83/2.03 0 [] p3(f12(c62),f12(c60)).
% 1.83/2.03 0 [] p52(f20(f21(c62,c64)),c66).
% 1.83/2.03 0 [] p2(f22(c58,c60,c61),c62).
% 1.83/2.03 0 [] p47(X133)| -p47(X134)| -p2(X134,X133).
% 1.83/2.03 0 [] p48(X135)| -p48(X136)| -p2(X136,X135).
% 1.83/2.03 0 [] p49(f4(c62),f13(f14(c63),f4(c60))).
% 1.83/2.03 0 [] -p50(c66,f25(f27(c59,c68),c67),c60).
% 1.83/2.03 0 [] p40(f41(X118),f41(X119))| -p15(X118,X119).
% 1.83/2.03 0 [] p10(f11(X3),f11(X4))| -p2(X3,X4).
% 1.83/2.03 0 [] p10(f31(X5),f31(X6))| -p30(X5,X6).
% 1.83/2.03 0 [] p15(f38(X10),f38(X11))| -p15(X10,X11).
% 1.83/2.03 0 [] p16(f17(X21),f17(X22))| -p15(X21,X22).
% 1.83/2.03 0 [] p19(f20(X33),f20(X34))| -p18(X33,X34).
% 1.83/2.03 0 [] p24(f39(X62),f39(X63))| -p15(X62,X63).
% 1.83/2.03 0 [] p3(f12(X83),f12(X84))| -p2(X83,X84).
% 1.83/2.03 0 [] p3(f14(X89),f14(X90))| -p3(X89,X90).
% 1.83/2.03 0 [] p3(f37(X91),f37(X92))| -p36(X91,X92).
% 1.83/2.03 0 [] p3(f4(X93),f4(X94))| -p2(X93,X94).
% 1.83/2.03 0 [] p10(X1,X2)| -p10(X0,X1)| -p10(X0,X2).
% 1.83/2.03 0 [] p7(X202,X203)| -p7(X201,X202)| -p7(X201,X203).
% 1.83/2.03 0 [] p5(X142,X143)| -p5(X141,X142)| -p5(X141,X143).
% 1.83/2.03 0 [] p42(X121,X122)| -p42(X120,X121)| -p42(X120,X122).
% 1.83/2.03 0 [] p40(X116,X117)| -p40(X115,X116)| -p40(X115,X117).
% 1.83/2.03 0 [] p36(X113,X114)| -p36(X112,X113)| -p36(X112,X114).
% 1.83/2.03 0 [] p33(X106,X107)| -p33(X105,X106)| -p33(X105,X107).
% 1.83/2.03 0 [] p32(X99,X100)| -p32(X98,X99)| -p32(X98,X100).
% 1.83/2.03 0 [] p30(X96,X97)| -p30(X95,X96)| -p30(X95,X97).
% 1.83/2.03 0 [] p3(X81,X82)| -p3(X80,X81)| -p3(X80,X82).
% 1.83/2.03 0 [] p28(X74,X75)| -p28(X73,X74)| -p28(X73,X75).
% 1.83/2.03 0 [] p26(X65,X66)| -p26(X64,X65)| -p26(X64,X66).
% 1.83/2.03 0 [] p24(X56,X57)| -p24(X55,X56)| -p24(X55,X57).
% 1.83/2.03 0 [] p23(X49,X50)| -p23(X48,X49)| -p23(X48,X50).
% 1.83/2.03 0 [] p2(X36,X37)| -p2(X35,X36)| -p2(X35,X37).
% 1.83/2.03 0 [] p19(X31,X32)| -p19(X30,X31)| -p19(X30,X32).
% 1.83/2.03 0 [] p18(X24,X25)| -p18(X23,X24)| -p18(X23,X25).
% 1.83/2.03 0 [] p16(X13,X14)| -p16(X12,X13)| -p16(X12,X14).
% 1.83/2.03 0 [] p15(X8,X9)| -p15(X7,X8)| -p15(X7,X9).
% 1.83/2.03 0 [] p50(c66,f25(f27(c59,X160),c67),c62)| -p53(X160,f17(c66)).
% 1.83/2.03 0 [] p57(X197,X198)| -p5(X200,X198)| -p57(X199,X200)| -p5(X199,X197).
% 1.83/2.03 0 [] p45(X125,X126)| -p5(X127,X125)| -p5(X128,X126)| -p45(X127,X128).
% 1.83/2.03 0 [] p46(X129,X130)| -p46(X132,X131)| -p7(X132,X129)| -p3(X131,X130).
% 1.83/2.03 0 [] p49(X137,X138)| -p3(X140,X138)| -p49(X139,X140)| -p3(X139,X137).
% 1.83/2.03 0 [] p51(X161,X162)| -p24(X164,X162)| -p51(X163,X164)| -p15(X163,X161).
% 1.83/2.03 0 [] p52(X169,X170)| -p19(X172,X169)| -p52(X172,X171)| -p15(X171,X170).
% 1.83/2.03 0 [] p53(X173,X174)| -p26(X176,X173)| -p53(X176,X175)| -p16(X175,X174).
% 1.83/2.03 0 [] p54(X177,X178)| -p30(X180,X177)| -p54(X180,X179)| -p28(X179,X178).
% 1.83/2.03 0 [] p55(X185,X186)| -p5(X188,X185)| -p55(X188,X187)| -p10(X187,X186).
% 1.83/2.03 0 [] p56(X189,X190)| -p36(X192,X189)| -p56(X192,X191)| -p33(X191,X190).
% 1.83/2.03 0 [] p45(X123,c61)| -p46(f8(f9(c58,X123),X124),f4(f6(c59,c60))).
% 1.83/2.03 0 [] p7(f8(X204,X205),f8(X206,X207))| -p5(X204,X206)| -p5(X205,X207).
% 1.83/2.03 0 [] p18(f21(X26,X27),f21(X28,X29))| -p18(X27,X29)| -p2(X26,X28).
% 1.83/2.03 0 [] p2(f6(X44,X45),f6(X46,X47))| -p2(X45,X47)| -p5(X44,X46).
% 1.83/2.03 0 [] p23(f27(X51,X52),f27(X53,X54))| -p26(X52,X54)| -p5(X51,X53).
% 1.83/2.03 0 [] p24(f25(X58,X59),f25(X60,X61))| -p23(X58,X60)| -p24(X59,X61).
% 1.83/2.03 0 [] p28(f29(X76,X77),f29(X78,X79))| -p28(X77,X79)| -p7(X76,X78).
% 1.83/2.03 0 [] p3(f13(X85,X86),f13(X87,X88))| -p3(X85,X87)| -p3(X86,X88).
% 1.83/2.03 0 [] p32(f35(X101,X102),f35(X103,X104))| -p5(X101,X103)| -p7(X102,X104).
% 1.83/2.03 0 [] p33(f34(X108,X109),f34(X110,X111))| -p32(X108,X110)| -p33(X109,X111).
% 1.83/2.03 0 [] p5(f9(X150,X151),f9(X152,X153))| -p5(X150,X152)| -p5(X151,X153).
% 1.83/2.03 0 [] p56(X193,f34(f35(X194,X195),X196))| -p56(X193,X196)| -p46(X195,f37(X193)).
% 1.83/2.03 0 [] p51(X165,f25(f27(X166,X167),X168))| -p51(X165,X168)| -p53(X167,f17(X165)).
% 1.83/2.03 0 [] p54(X181,f29(f8(X182,X183),X184))| -p54(X181,X184)| -p55(X183,f31(X181)).
% 1.83/2.03 0 [] p50(X154,X155,X156)| -p15(X157,X154)| -p2(X158,X156)| -p24(X159,X155)| -p50(X157,X159,X158).
% 1.83/2.03 0 [] p2(f22(X38,X39,X40),f22(X41,X42,X43))| -p5(X38,X41)| -p5(X40,X43)| -p2(X39,X42).
% 1.83/2.03 0 [] p5(f43(X144,X145,X146),f43(X147,X148,X149))| -p42(X146,X149)| -p5(X145,X148)| -p15(X144,X147).
% 1.83/2.03 0 [] p26(f44(X67,X68,X69),f44(X70,X71,X72))| -p42(X69,X72)| -p5(X68,X71)| -p15(X67,X70).
% 1.83/2.03 0 [] p51(X17,f39(X17))|p16(f17(X17),c65)|p16(f17(f38(X17)),f17(X17))| -p52(f20(f21(c60,c64)),X17).
% 1.83/2.03 0 [] p51(X17,f39(X17))|p16(f17(X17),c65)|p40(f41(f38(X17)),f41(X17))| -p52(f20(f21(c60,c64)),X17).
% 1.83/2.03 0 [] p51(X17,f39(X17))|p16(f17(X17),c65)|p52(f20(f21(c62,c64)),f38(X17))| -p52(f20(f21(c60,c64)),X17).
% 1.83/2.03 0 [] p16(f17(X17),c65)|p16(f17(f38(X17)),f17(X17))| -p50(X17,f39(X17),c60)| -p52(f20(f21(c60,c64)),X17).
% 1.83/2.03 0 [] p16(f17(X17),c65)|p40(f41(f38(X17)),f41(X17))| -p50(X17,f39(X17),c60)| -p52(f20(f21(c60,c64)),X17).
% 1.83/2.03 0 [] p16(f17(X15),c65)|p50(X15,X16,c60)| -p51(X15,X16)| -p50(X15,X16,c62)| -p52(f20(f21(c62,c64)),X15).
% 1.83/2.03 0 [] p16(f17(X17),c65)|p52(f20(f21(c62,c64)),f38(X17))| -p50(X17,f39(X17),c60)| -p52(f20(f21(c60,c64)),X17).
% 1.83/2.03 0 [] p51(X17,f39(X17))|p16(f17(X17),c65)|p50(f38(X17),X20,c62)| -p51(f38(X17),X20)| -p52(f20(f21(c60,c64)),X17).
% 1.83/2.03 0 [] p16(f17(X17),c65)|p50(f38(X17),X20,c62)| -p51(f38(X17),X20)| -p50(X17,f39(X17),c60)| -p52(f20(f21(c60,c64)),X17).
% 1.83/2.03 0 [] p51(X17,f39(X17))|p16(f17(X17),c65)|p57(c61,f43(X17,X18,X19))|p26(f44(f38(X17),X18,X19),f44(X17,X18,X19))| -p52(f20(f21(c60,c64)),X17).
% 1.83/2.03 0 [] p16(f17(X17),c65)|p57(c61,f43(X17,X18,X19))|p26(f44(f38(X17),X18,X19),f44(X17,X18,X19))| -p50(X17,f39(X17),c60)| -p52(f20(f21(c60,c64)),X17).
% 1.83/2.03 0 [] p51(X17,f39(X17))|p16(f17(X17),c65)|p5(X18,f9(c58,f43(X17,X18,X19)))|p26(f44(f38(X17),X18,X19),f44(X17,X18,X19))| -p52(f20(f21(c60,c64)),X17).
% 1.83/2.03 0 [] p16(f17(X17),c65)|p5(X18,f9(c58,f43(X17,X18,X19)))|p26(f44(f38(X17),X18,X19),f44(X17,X18,X19))| -p50(X17,f39(X17),c60)| -p52(f20(f21(c60,c64)),X17).
% 1.83/2.03 end_of_list.
% 1.83/2.03
% 1.83/2.03 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=5.
% 1.83/2.03
% 1.83/2.03 This is a non-Horn set without equality. The strategy will
% 1.83/2.03 be ordered hyper_res, unit deletion, and factoring, with
% 1.83/2.03 satellites in sos and with nuclei in usable.
% 1.83/2.03
% 1.83/2.03 dependent: set(hyper_res).
% 1.83/2.03 dependent: set(factor).
% 1.83/2.03 dependent: set(unit_deletion).
% 1.83/2.03
% 1.83/2.03 ------------> process usable:
% 1.83/2.03 ** KEPT (pick-wt=4): 1 [] -p16(f17(c66),c65).
% 1.83/2.03 ** KEPT (pick-wt=7): 2 [] p47(A)| -p47(B)| -p2(B,A).
% 1.83/2.03 ** KEPT (pick-wt=7): 3 [] p48(A)| -p48(B)| -p2(B,A).
% 1.83/2.03 ** KEPT (pick-wt=8): 4 [] -p50(c66,f25(f27(c59,c68),c67),c60).
% 1.83/2.03 ** KEPT (pick-wt=8): 5 [] p40(f41(A),f41(B))| -p15(A,B).
% 1.83/2.03 ** KEPT (pick-wt=8): 6 [] p10(f11(A),f11(B))| -p2(A,B).
% 1.83/2.03 ** KEPT (pick-wt=8): 7 [] p10(f31(A),f31(B))| -p30(A,B).
% 1.83/2.03 ** KEPT (pick-wt=8): 8 [] p15(f38(A),f38(B))| -p15(A,B).
% 1.83/2.03 ** KEPT (pick-wt=8): 9 [] p16(f17(A),f17(B))| -p15(A,B).
% 1.83/2.03 ** KEPT (pick-wt=8): 10 [] p19(f20(A),f20(B))| -p18(A,B).
% 1.83/2.03 ** KEPT (pick-wt=8): 11 [] p24(f39(A),f39(B))| -p15(A,B).
% 1.83/2.03 ** KEPT (pick-wt=8): 12 [] p3(f12(A),f12(B))| -p2(A,B).
% 1.83/2.03 ** KEPT (pick-wt=8): 13 [] p3(f14(A),f14(B))| -p3(A,B).
% 1.83/2.03 ** KEPT (pick-wt=8): 14 [] p3(f37(A),f37(B))| -p36(A,B).
% 1.83/2.03 ** KEPT (pick-wt=8): 15 [] p3(f4(A),f4(B))| -p2(A,B).
% 1.83/2.03 ** KEPT (pick-wt=9): 16 [] p10(A,B)| -p10(C,A)| -p10(C,B).
% 1.83/2.03 ** KEPT (pick-wt=9): 17 [] p7(A,B)| -p7(C,A)| -p7(C,B).
% 1.83/2.03 ** KEPT (pick-wt=9): 18 [] p5(A,B)| -p5(C,A)| -p5(C,B).
% 1.83/2.03 ** KEPT (pick-wt=9): 19 [] p42(A,B)| -p42(C,A)| -p42(C,B).
% 1.83/2.03 ** KEPT (pick-wt=9): 20 [] p40(A,B)| -p40(C,A)| -p40(C,B).
% 1.83/2.03 ** KEPT (pick-wt=9): 21 [] p36(A,B)| -p36(C,A)| -p36(C,B).
% 1.83/2.03 ** KEPT (pick-wt=9): 22 [] p33(A,B)| -p33(C,A)| -p33(C,B).
% 1.83/2.03 ** KEPT (pick-wt=9): 23 [] p32(A,B)| -p32(C,A)| -p32(C,B).
% 1.83/2.03 ** KEPT (pick-wt=9): 24 [] p30(A,B)| -p30(C,A)| -p30(C,B).
% 1.83/2.03 ** KEPT (pick-wt=9): 25 [] p3(A,B)| -p3(C,A)| -p3(C,B).
% 1.83/2.03 ** KEPT (pick-wt=9): 26 [] p28(A,B)| -p28(C,A)| -p28(C,B).
% 1.83/2.03 ** KEPT (pick-wt=9): 27 [] p26(A,B)| -p26(C,A)| -p26(C,B).
% 1.83/2.03 ** KEPT (pick-wt=9): 28 [] p24(A,B)| -p24(C,A)| -p24(C,B).
% 1.83/2.03 ** KEPT (pick-wt=9): 29 [] p23(A,B)| -p23(C,A)| -p23(C,B).
% 1.83/2.03 ** KEPT (pick-wt=9): 30 [] p2(A,B)| -p2(C,A)| -p2(C,B).
% 1.83/2.03 ** KEPT (pick-wt=9): 31 [] p19(A,B)| -p19(C,A)| -p19(C,B).
% 1.83/2.03 ** KEPT (pick-wt=9): 32 [] p18(A,B)| -p18(C,A)| -p18(C,B).
% 1.83/2.03 ** KEPT (pick-wt=9): 33 [] p16(A,B)| -p16(C,A)| -p16(C,B).
% 1.83/2.03 ** KEPT (pick-wt=9): 34 [] p15(A,B)| -p15(C,A)| -p15(C,B).
% 1.83/2.03 ** KEPT (pick-wt=12): 35 [] p50(c66,f25(f27(c59,A),c67),c62)| -p53(A,f17(c66)).
% 1.83/2.03 ** KEPT (pick-wt=12): 36 [] p57(A,B)| -p5(C,B)| -p57(D,C)| -p5(D,A).
% 1.83/2.03 ** KEPT (pick-wt=12): 37 [] p45(A,B)| -p5(C,A)| -p5(D,B)| -p45(C,D).
% 1.83/2.03 ** KEPT (pick-wt=12): 38 [] p46(A,B)| -p46(C,D)| -p7(C,A)| -p3(D,B).
% 1.83/2.03 ** KEPT (pick-wt=12): 39 [] p49(A,B)| -p3(C,B)| -p49(D,C)| -p3(D,A).
% 1.83/2.03 ** KEPT (pick-wt=12): 40 [] p51(A,B)| -p24(C,B)| -p51(D,C)| -p15(D,A).
% 1.83/2.03 ** KEPT (pick-wt=12): 41 [] p52(A,B)| -p19(C,A)| -p52(C,D)| -p15(D,B).
% 1.83/2.03 ** KEPT (pick-wt=12): 42 [] p53(A,B)| -p26(C,A)| -p53(C,D)| -p16(D,B).
% 1.83/2.03 ** KEPT (pick-wt=12): 43 [] p54(A,B)| -p30(C,A)| -p54(C,D)| -p28(D,B).
% 1.83/2.03 ** KEPT (pick-wt=12): 44 [] p55(A,B)| -p5(C,A)| -p55(C,D)| -p10(D,B).
% 1.83/2.03 ** KEPT (pick-wt=12): 45 [] p56(A,B)| -p36(C,A)| -p56(C,D)| -p33(D,B).
% 1.83/2.03 ** KEPT (pick-wt=13): 46 [] p45(A,c61)| -p46(f8(f9(c58,A),B),f4(f6(c59,c60))).
% 1.83/2.03 ** KEPT (pick-wt=13): 47 [] p7(f8(A,B),f8(C,D))| -p5(A,C)| -p5(B,D).
% 1.83/2.03 ** KEPT (pick-wt=13): 48 [] p18(f21(A,B),f21(C,D))| -p18(B,D)| -p2(A,C).
% 1.83/2.03 ** KEPT (pick-wt=13): 49 [] p2(f6(A,B),f6(C,D))| -p2(B,D)| -p5(A,C).
% 1.83/2.03 ** KEPT (pick-wt=13): 50 [] p23(f27(A,B),f27(C,D))| -p26(B,D)| -p5(A,C).
% 1.83/2.03 ** KEPT (pick-wt=13): 51 [] p24(f25(A,B),f25(C,D))| -p23(A,C)| -p24(B,D).
% 1.83/2.03 ** KEPT (pick-wt=13): 52 [] p28(f29(A,B),f29(C,D))| -p28(B,D)| -p7(A,C).
% 1.83/2.03 ** KEPT (pick-wt=13): 53 [] p3(f13(A,B),f13(C,D))| -p3(A,C)| -p3(B,D).
% 1.83/2.03 ** KEPT (pick-wt=13): 54 [] p32(f35(A,B),f35(C,D))| -p5(A,C)| -p7(B,D).
% 1.83/2.03 ** KEPT (pick-wt=13): 55 [] p33(f34(A,B),f34(C,D))| -p32(A,C)| -p33(B,D).
% 1.83/2.03 ** KEPT (pick-wt=13): 56 [] p5(f9(A,B),f9(C,D))| -p5(A,C)| -p5(B,D).
% 1.83/2.03 ** KEPT (pick-wt=14): 57 [] p56(A,f34(f35(B,C),D))| -p56(A,D)| -p46(C,f37(A)).
% 1.83/2.03 ** KEPT (pick-wt=14): 58 [] p51(A,f25(f27(B,C),D))| -p51(A,D)| -p53(C,f17(A)).
% 1.83/2.03 ** KEPT (pick-wt=14): 59 [] p54(A,f29(f8(B,C),D))| -p54(A,D)| -p55(C,f31(A)).
% 1.83/2.03 ** KEPT (pick-wt=17): 60 [] p50(A,B,C)| -p15(D,A)| -p2(E,C)| -p24(F,B)| -p50(D,F,E).
% 1.83/2.03 ** KEPT (pick-wt=18): 61 [] p2(f22(A,B,C),f22(D,E,F))| -p5(A,D)| -p5(C,F)| -p2(B,E).
% 1.83/2.03 ** KEPT (pick-wt=18): 62 [] p5(f43(A,B,C),f43(D,E,F))| -p42(C,F)| -p5(B,E)| -p15(A,D).
% 1.83/2.03 ** KEPT (pick-wt=18): 63 [] p26(f44(A,B,C),f44(D,E,F))| -p42(C,F)| -p5(B,E)| -p15(A,D).
% 1.83/2.03 ** KEPT (pick-wt=20): 64 [] p51(A,f39(A))|p16(f17(A),c65)|p16(f17(f38(A)),f17(A))| -p52(f20(f21(c60,c64)),A).
% 1.83/2.03 ** KEPT (pick-wt=20): 65 [] p51(A,f39(A))|p16(f17(A),c65)|p40(f41(f38(A)),f41(A))| -p52(f20(f21(c60,c64)),A).
% 1.83/2.03 ** KEPT (pick-wt=21): 66 [] p51(A,f39(A))|p16(f17(A),c65)|p52(f20(f21(c62,c64)),f38(A))| -p52(f20(f21(c60,c64)),A).
% 1.83/2.03 ** KEPT (pick-wt=21): 67 [] p16(f17(A),c65)|p16(f17(f38(A)),f17(A))| -p50(A,f39(A),c60)| -p52(f20(f21(c60,c64)),A).
% 1.83/2.03 ** KEPT (pick-wt=21): 68 [] p16(f17(A),c65)|p40(f41(f38(A)),f41(A))| -p50(A,f39(A),c60)| -p52(f20(f21(c60,c64)),A).
% 1.83/2.03 ** KEPT (pick-wt=21): 69 [] p16(f17(A),c65)|p50(A,B,c60)| -p51(A,B)| -p50(A,B,c62)| -p52(f20(f21(c62,c64)),A).
% 1.83/2.03 ** KEPT (pick-wt=22): 70 [] p16(f17(A),c65)|p52(f20(f21(c62,c64)),f38(A))| -p50(A,f39(A),c60)| -p52(f20(f21(c60,c64)),A).
% 1.83/2.03 ** KEPT (pick-wt=23): 71 [] p51(A,f39(A))|p16(f17(A),c65)|p50(f38(A),B,c62)| -p51(f38(A),B)| -p52(f20(f21(c60,c64)),A).
% 1.83/2.03 ** KEPT (pick-wt=24): 72 [] p16(f17(A),c65)|p50(f38(A),B,c62)| -p51(f38(A),B)| -p50(A,f39(A),c60)| -p52(f20(f21(c60,c64)),A).
% 1.83/2.03 ** KEPT (pick-wt=30): 73 [] p51(A,f39(A))|p16(f17(A),c65)|p57(c61,f43(A,B,C))|p26(f44(f38(A),B,C),f44(A,B,C))| -p52(f20(f21(c60,c64)),A).
% 1.83/2.03 ** KEPT (pick-wt=31): 74 [] p16(f17(A),c65)|p57(c61,f43(A,B,C))|p26(f44(f38(A),B,C),f44(A,B,C))| -p50(A,f39(A),c60)| -p52(f20(f21(c60,c64)),A).
% 1.83/2.04 ** KEPT (pick-wt=32): 75 [] p51(A,f39(A))|p16(f17(A),c65)|p5(B,f9(c58,f43(A,B,C)))|p26(f44(f38(A),B,C),f44(A,B,C))| -p52(f20(f21(c60,c64)),A).
% 1.83/2.04 ** KEPT (pick-wt=33): 76 [] p16(f17(A),c65)|p5(B,f9(c58,f43(A,B,C)))|p26(f44(f38(A),B,C),f44(A,B,C))| -p50(A,f39(A),c60)| -p52(f20(f21(c60,c64)),A).
% 1.83/2.04
% 1.83/2.04 ------------> process sos:
% 1.83/2.04 ** KEPT (pick-wt=2): 103 [] p48(c62).
% 1.83/2.04 ** KEPT (pick-wt=2): 104 [] p47(c60).
% 1.83/2.04 ** KEPT (pick-wt=3): 105 [] p10(A,A).
% 1.83/2.04 ** KEPT (pick-wt=3): 106 [] p7(A,A).
% 1.83/2.04 ** KEPT (pick-wt=3): 107 [] p5(A,A).
% 1.83/2.04 ** KEPT (pick-wt=3): 108 [] p42(A,A).
% 1.83/2.04 ** KEPT (pick-wt=3): 109 [] p40(A,A).
% 1.83/2.04 ** KEPT (pick-wt=3): 110 [] p36(A,A).
% 1.83/2.04 ** KEPT (pick-wt=3): 111 [] p33(A,A).
% 1.83/2.04 ** KEPT (pick-wt=3): 112 [] p32(A,A).
% 1.83/2.04 ** KEPT (pick-wt=3): 113 [] p30(A,A).
% 1.83/2.04 ** KEPT (pick-wt=3): 114 [] p3(A,A).
% 1.83/2.04 ** KEPT (pick-wt=3): 115 [] p28(A,A).
% 1.83/2.04 ** KEPT (pick-wt=3): 116 [] p26(A,A).
% 1.83/2.04 ** KEPT (pick-wt=3): 117 [] p24(A,A).
% 1.83/2.04 ** KEPT (pick-wt=3): 118 [] p23(A,A).
% 1.83/2.04 ** KEPT (pick-wt=3): 119 [] p2(A,A).
% 1.83/2.04 ** KEPT (pick-wt=3): 120 [] p19(A,A).
% 1.83/2.04 ** KEPT (pick-wt=3): 121 [] p18(A,A).
% 1.83/2.04 ** KEPT (pick-wt=3): 122 [] p16(A,A).
% 1.83/2.04 ** KEPT (pick-wt=3): 123 [] p15(A,A).
% 1.83/2.04 ** KEPT (pick-wt=3): 124 [] p51(c66,c67).
% 1.83/2.04 ** KEPT (pick-wt=4): 125 [] p53(c68,f17(c66)).
% 1.83/2.04 ** KEPT (pick-wt=5): 126 [] p10(f11(c62),f11(c60)).
% 1.83/2.04 ** KEPT (pick-wt=5): 127 [] p49(f4(c60),f4(c62)).
% 1.83/2.04 ** KEPT (pick-wt=5): 128 [] p3(f12(c62),f12(c60)).
% 1.83/2.04 ** KEPT (pick-wt=6): 129 [] p52(f20(f21(c62,c64)),c66).
% 1.83/2.04 ** KEPT (pick-wt=6): 130 [] p2(f22(c58,c60,c61),c62).
% 1.83/2.04 ** KEPT (pick-wt=8): 131 [] p49(f4(c62),f13(f14(c63),f4(c60))).
% 1.83/2.04 105 back subsumes 77.
% 1.83/2.04 106 back subsumes 78.
% 1.83/2.04 107 back subsumes 79.
% 1.83/2.04 108 back subsumes 80.
% 1.83/2.04 109 back subsumes 81.
% 1.83/2.04 110 back subsumes 82.
% 1.83/2.04 111 back subsumes 83.
% 1.83/2.04 112 back subsumes 84.
% 1.83/2.04 113 back subsumes 85.
% 1.83/2.04 114 back subsumes 86.
% 1.83/2.04 115 back subsumes 87.
% 1.83/2.04 116 back subsumes 88.
% 1.83/2.04 117 back subsumes 89.
% 1.83/2.04 118 back subsumes 90.
% 1.83/2.04 119 back subsumes 91.
% 1.83/2.04 120 back subsumes 92.
% 1.83/2.04 121 back subsumes 93.
% 1.83/2.04 122 back subsumes 94.
% 1.83/2.04 123 back subsumes 95.
% 1.83/2.04
% 1.83/2.04 ======= end of input processing =======
% 1.83/2.04
% 1.83/2.04 =========== start of search ===========
% 1.83/2.04
% 1.83/2.04 -------- PROOF --------
% 1.83/2.04
% 1.83/2.04 -----> EMPTY CLAUSE at 0.01 sec ----> 171 [hyper,133,69,132,129,unit_del,1,4] $F.
% 1.83/2.04
% 1.83/2.04 Length of proof is 2. Level of proof is 1.
% 1.83/2.04
% 1.83/2.04 ---------------- PROOF ----------------
% 1.83/2.04 % SZS status Unsatisfiable
% 1.83/2.04 % SZS output start Refutation
% See solution above
% 1.83/2.04 ------------ end of proof -------------
% 1.83/2.04
% 1.83/2.04
% 1.83/2.04 Search stopped by max_proofs option.
% 1.83/2.04
% 1.83/2.04
% 1.83/2.04 Search stopped by max_proofs option.
% 1.83/2.04
% 1.83/2.04 ============ end of search ============
% 1.83/2.04
% 1.83/2.04 -------------- statistics -------------
% 1.83/2.04 clauses given 36
% 1.83/2.04 clauses generated 176
% 1.83/2.04 clauses kept 170
% 1.83/2.04 clauses forward subsumed 110
% 1.83/2.04 clauses back subsumed 21
% 1.83/2.04 Kbytes malloced 1953
% 1.83/2.04
% 1.83/2.04 ----------- times (seconds) -----------
% 1.83/2.04 user CPU time 0.01 (0 hr, 0 min, 0 sec)
% 1.83/2.04 system CPU time 0.00 (0 hr, 0 min, 0 sec)
% 1.83/2.04 wall-clock time 1 (0 hr, 0 min, 1 sec)
% 1.83/2.04
% 1.83/2.04 That finishes the proof of the theorem.
% 1.83/2.04
% 1.83/2.04 Process 15310 finished Wed Jul 27 11:28:38 2022
% 1.83/2.04 Otter interrupted
% 1.83/2.04 PROOF FOUND
%------------------------------------------------------------------------------