%------------------------------------------------------------------------------
% File : Otter---3.3
% Problem : SYN037-1 : TPTP v8.1.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : otter-tptp-script %s
% Computer : n014.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:23:21 EDT 2022
% Result : Unsatisfiable 1.87s 2.05s
% Output : Refutation 1.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 61
% Number of leaves : 35
% Syntax : Number of clauses : 119 ( 14 unt; 80 nHn; 87 RR)
% Number of literals : 291 ( 0 equ; 50 neg)
% Maximal clause size : 4 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 13 ( 12 usr; 9 prp; 0-1 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-1 aty)
% Number of variables : 44 ( 34 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
( ~ n2
| ~ n9
| ~ n6
| ~ n10 ),
file('SYN037-1.p',unknown),
[] ).
cnf(2,axiom,
( ~ n2
| ~ n9
| n6
| n10 ),
file('SYN037-1.p',unknown),
[] ).
cnf(3,axiom,
( n2
| n9
| ~ n6
| ~ n10 ),
file('SYN037-1.p',unknown),
[] ).
cnf(4,axiom,
( ~ n2
| n9
| ~ n6
| n10 ),
file('SYN037-1.p',unknown),
[] ).
cnf(5,axiom,
( ~ n2
| n9
| n6
| ~ n10 ),
file('SYN037-1.p',unknown),
[] ).
cnf(6,axiom,
( n2
| ~ n9
| ~ n6
| n10 ),
file('SYN037-1.p',unknown),
[] ).
cnf(8,axiom,
( ~ q(s8)
| n8 ),
file('SYN037-1.p',unknown),
[] ).
cnf(9,axiom,
( ~ n8
| q(A) ),
file('SYN037-1.p',unknown),
[] ).
cnf(10,axiom,
( ~ p(A)
| n7 ),
file('SYN037-1.p',unknown),
[] ).
cnf(11,axiom,
( ~ n7
| p(s7) ),
file('SYN037-1.p',unknown),
[] ).
cnf(12,axiom,
( ~ n5(A)
| n6 ),
file('SYN037-1.p',unknown),
[] ).
cnf(13,axiom,
( ~ n6
| n5(s6) ),
file('SYN037-1.p',unknown),
[] ).
cnf(14,axiom,
( ~ q(s5(A))
| ~ q(A)
| n5(A) ),
file('SYN037-1.p',unknown),
[] ).
cnf(15,axiom,
( ~ n5(A)
| ~ q(B)
| q(A) ),
file('SYN037-1.p',unknown),
[] ).
cnf(16,axiom,
( ~ n5(A)
| q(B)
| ~ q(A) ),
file('SYN037-1.p',unknown),
[] ).
cnf(17,axiom,
( ~ p(s4)
| n4 ),
file('SYN037-1.p',unknown),
[] ).
cnf(18,axiom,
( ~ n4
| p(A) ),
file('SYN037-1.p',unknown),
[] ).
cnf(19,axiom,
( ~ q(A)
| n3 ),
file('SYN037-1.p',unknown),
[] ).
cnf(20,axiom,
( ~ n3
| q(s3) ),
file('SYN037-1.p',unknown),
[] ).
cnf(21,axiom,
( ~ n1(A)
| n2 ),
file('SYN037-1.p',unknown),
[] ).
cnf(22,axiom,
( ~ n2
| n1(s2) ),
file('SYN037-1.p',unknown),
[] ).
cnf(23,axiom,
( ~ p(A)
| ~ p(s1(A))
| n1(A) ),
file('SYN037-1.p',unknown),
[] ).
cnf(24,axiom,
( ~ n1(A)
| ~ p(A)
| p(B) ),
file('SYN037-1.p',unknown),
[] ).
cnf(25,axiom,
( ~ n1(A)
| p(A)
| ~ p(B) ),
file('SYN037-1.p',unknown),
[] ).
cnf(26,axiom,
( ~ n3
| ~ n4
| n9 ),
file('SYN037-1.p',unknown),
[] ).
cnf(27,axiom,
( ~ n3
| n4
| ~ n9 ),
file('SYN037-1.p',unknown),
[] ).
cnf(28,axiom,
( n3
| ~ n4
| ~ n9 ),
file('SYN037-1.p',unknown),
[] ).
cnf(29,axiom,
( ~ n7
| ~ n8
| n10 ),
file('SYN037-1.p',unknown),
[] ).
cnf(30,axiom,
( ~ n7
| n8
| ~ n10 ),
file('SYN037-1.p',unknown),
[] ).
cnf(31,axiom,
( n7
| ~ n8
| ~ n10 ),
file('SYN037-1.p',unknown),
[] ).
cnf(32,axiom,
( n2
| n9
| n6
| n10 ),
file('SYN037-1.p',unknown),
[] ).
cnf(33,axiom,
( q(s5(A))
| q(A)
| n5(A) ),
file('SYN037-1.p',unknown),
[] ).
cnf(34,axiom,
( p(A)
| p(s1(A))
| n1(A) ),
file('SYN037-1.p',unknown),
[] ).
cnf(35,axiom,
( n3
| n4
| n9 ),
file('SYN037-1.p',unknown),
[] ).
cnf(36,axiom,
( n7
| n8
| n10 ),
file('SYN037-1.p',unknown),
[] ).
cnf(37,plain,
( n7
| n10
| q(A) ),
inference(hyper,[status(thm)],[36,9]),
[iquote('hyper,36,9')] ).
cnf(38,plain,
( n7
| n10
| n3 ),
inference(hyper,[status(thm)],[37,19]),
[iquote('hyper,37,19')] ).
cnf(39,plain,
( n7
| n10
| n5(A) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[37,14,37])])]),
[iquote('hyper,37,14,37,factor_simp,factor_simp')] ).
cnf(40,plain,
( n10
| n3
| p(s7) ),
inference(hyper,[status(thm)],[38,11]),
[iquote('hyper,38,11')] ).
cnf(41,plain,
( q(A)
| n5(A)
| n3 ),
inference(hyper,[status(thm)],[33,19]),
[iquote('hyper,33,19')] ).
cnf(45,plain,
( n7
| n10
| n6 ),
inference(hyper,[status(thm)],[39,12]),
[iquote('hyper,39,12')] ).
cnf(46,plain,
( n10
| n6
| p(s7) ),
inference(hyper,[status(thm)],[45,11]),
[iquote('hyper,45,11')] ).
cnf(52,plain,
( p(A)
| n1(A)
| n7 ),
inference(hyper,[status(thm)],[34,10]),
[iquote('hyper,34,10')] ).
cnf(53,plain,
( n5(A)
| n3 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[41,19])]),
[iquote('hyper,41,19,factor_simp')] ).
cnf(54,plain,
( n3
| n6 ),
inference(hyper,[status(thm)],[53,12]),
[iquote('hyper,53,12')] ).
cnf(55,plain,
( n3
| n2
| n10
| n4 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[54,6,35])]),
[iquote('hyper,54,6,35,factor_simp')] ).
cnf(56,plain,
( n3
| n2
| n10
| p(A) ),
inference(hyper,[status(thm)],[55,18]),
[iquote('hyper,55,18')] ).
cnf(62,plain,
( n1(A)
| n7 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[52,10])]),
[iquote('hyper,52,10,factor_simp')] ).
cnf(63,plain,
( n7
| n2 ),
inference(hyper,[status(thm)],[62,21]),
[iquote('hyper,62,21')] ).
cnf(68,plain,
( n3
| n2
| n10
| n1(A) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[56,23,56])])])]),
[iquote('hyper,56,23,56,factor_simp,factor_simp,factor_simp')] ).
cnf(69,plain,
( n3
| n2
| n10 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[68,21])]),
[iquote('hyper,68,21,factor_simp')] ).
cnf(70,plain,
( n2
| n10
| n4
| n6 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[69,27,32])])]),
[iquote('hyper,69,27,32,factor_simp,factor_simp')] ).
cnf(71,plain,
( n2
| n10
| q(s3) ),
inference(hyper,[status(thm)],[69,20]),
[iquote('hyper,69,20')] ).
cnf(72,plain,
( n2
| n10
| n4
| n5(s6) ),
inference(hyper,[status(thm)],[70,13]),
[iquote('hyper,70,13')] ).
cnf(76,plain,
( n2
| n10
| n4
| q(s6) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[72,15,71])])]),
[iquote('hyper,72,15,71,factor_simp,factor_simp')] ).
cnf(77,plain,
( n2
| n10
| n4
| q(A) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[76,16,72])])])]),
[iquote('hyper,76,16,72,factor_simp,factor_simp,factor_simp')] ).
cnf(79,plain,
( n2
| n10
| n4
| n8 ),
inference(hyper,[status(thm)],[77,8]),
[iquote('hyper,77,8')] ).
cnf(81,plain,
( n2
| n10
| n4 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[79,29,63])])]),
[iquote('hyper,79,29,63,factor_simp,factor_simp')] ).
cnf(83,plain,
( n2
| n10
| p(A) ),
inference(hyper,[status(thm)],[81,18]),
[iquote('hyper,81,18')] ).
cnf(84,plain,
( n2
| n10
| n1(A) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[83,23,83])])]),
[iquote('hyper,83,23,83,factor_simp,factor_simp')] ).
cnf(91,plain,
( n2
| n10 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[84,21])]),
[iquote('hyper,84,21,factor_simp')] ).
cnf(92,plain,
( n10
| n1(s2) ),
inference(hyper,[status(thm)],[91,22]),
[iquote('hyper,91,22')] ).
cnf(93,plain,
( n10
| n9
| n3 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[91,4,54])]),
[iquote('hyper,91,4,54,factor_simp')] ).
cnf(98,plain,
( n10
| p(s2)
| n6 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[92,25,46])]),
[iquote('hyper,92,25,46,factor_simp')] ).
cnf(99,plain,
( n10
| p(s2)
| n3 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[92,25,40])]),
[iquote('hyper,92,25,40,factor_simp')] ).
cnf(104,plain,
( n10
| n6
| p(A) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[98,24,92])]),
[iquote('hyper,98,24,92,factor_simp')] ).
cnf(105,plain,
( n10
| n3
| p(A) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[99,24,92])]),
[iquote('hyper,99,24,92,factor_simp')] ).
cnf(107,plain,
( n10
| n6
| n4 ),
inference(hyper,[status(thm)],[104,17]),
[iquote('hyper,104,17')] ).
cnf(109,plain,
( n10
| n4
| n9 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[107,4,91])])]),
[iquote('hyper,107,4,91,factor_simp,factor_simp')] ).
cnf(114,plain,
( n10
| n3
| n4 ),
inference(hyper,[status(thm)],[105,17]),
[iquote('hyper,105,17')] ).
cnf(115,plain,
( n10
| n3 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[114,28,93])])])]),
[iquote('hyper,114,28,93,factor_simp,factor_simp,factor_simp')] ).
cnf(116,plain,
( n10
| n4 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[115,27,109])])]),
[iquote('hyper,115,27,109,factor_simp,factor_simp')] ).
cnf(117,plain,
( n10
| q(s3) ),
inference(hyper,[status(thm)],[115,20]),
[iquote('hyper,115,20')] ).
cnf(121,plain,
( n10
| n9 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[116,26,115])]),
[iquote('hyper,116,26,115,factor_simp')] ).
cnf(122,plain,
( n10
| p(A) ),
inference(hyper,[status(thm)],[116,18]),
[iquote('hyper,116,18')] ).
cnf(123,plain,
( n10
| n6 ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[121,2,91])])]),
[iquote('hyper,121,2,91,factor_simp,factor_simp')] ).
cnf(124,plain,
( n10
| n5(s6) ),
inference(hyper,[status(thm)],[123,13]),
[iquote('hyper,123,13')] ).
cnf(131,plain,
( n10
| n7 ),
inference(hyper,[status(thm)],[122,10]),
[iquote('hyper,122,10')] ).
cnf(132,plain,
( n10
| q(s6) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[124,15,117])]),
[iquote('hyper,124,15,117,factor_simp')] ).
cnf(134,plain,
( n10
| q(A) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[132,16,124])]),
[iquote('hyper,132,16,124,factor_simp')] ).
cnf(136,plain,
( n10
| n8 ),
inference(hyper,[status(thm)],[134,8]),
[iquote('hyper,134,8')] ).
cnf(137,plain,
n10,
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[136,29,131])])]),
[iquote('hyper,136,29,131,factor_simp,factor_simp')] ).
cnf(138,plain,
( n8
| n2 ),
inference(hyper,[status(thm)],[137,30,63]),
[iquote('hyper,137,30,63')] ).
cnf(141,plain,
( n2
| q(A) ),
inference(hyper,[status(thm)],[138,9]),
[iquote('hyper,138,9')] ).
cnf(142,plain,
( n2
| n3 ),
inference(hyper,[status(thm)],[141,19]),
[iquote('hyper,141,19')] ).
cnf(143,plain,
( n2
| n5(A) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[141,14,141])]),
[iquote('hyper,141,14,141,factor_simp')] ).
cnf(148,plain,
( n2
| n6 ),
inference(hyper,[status(thm)],[143,12]),
[iquote('hyper,143,12')] ).
cnf(149,plain,
( n2
| n9 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[148,3,137])]),
[iquote('hyper,148,3,137,factor_simp')] ).
cnf(150,plain,
( n2
| n4 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[149,27,142])]),
[iquote('hyper,149,27,142,factor_simp')] ).
cnf(151,plain,
( n2
| p(A) ),
inference(hyper,[status(thm)],[150,18]),
[iquote('hyper,150,18')] ).
cnf(155,plain,
( n2
| n1(A) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[151,23,151])]),
[iquote('hyper,151,23,151,factor_simp')] ).
cnf(156,plain,
n2,
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[155,21])]),
[iquote('hyper,155,21,factor_simp')] ).
cnf(157,plain,
n1(s2),
inference(hyper,[status(thm)],[156,22]),
[iquote('hyper,156,22')] ).
cnf(158,plain,
( n9
| n6 ),
inference(hyper,[status(thm)],[156,5,137]),
[iquote('hyper,156,5,137')] ).
cnf(159,plain,
( n3
| n4 ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[156,1,35,54,137])]),
[iquote('hyper,156,1,35,54,137,factor_simp')] ).
cnf(170,plain,
( n3
| p(A) ),
inference(hyper,[status(thm)],[159,18]),
[iquote('hyper,159,18')] ).
cnf(172,plain,
( n3
| n7 ),
inference(hyper,[status(thm)],[170,10]),
[iquote('hyper,170,10')] ).
cnf(173,plain,
( n3
| n8 ),
inference(hyper,[status(thm)],[172,30,137]),
[iquote('hyper,172,30,137')] ).
cnf(175,plain,
( n3
| q(A) ),
inference(hyper,[status(thm)],[173,9]),
[iquote('hyper,173,9')] ).
cnf(176,plain,
n3,
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[175,19])]),
[iquote('hyper,175,19,factor_simp')] ).
cnf(177,plain,
( n4
| n6 ),
inference(hyper,[status(thm)],[176,27,158]),
[iquote('hyper,176,27,158')] ).
cnf(178,plain,
q(s3),
inference(hyper,[status(thm)],[176,20]),
[iquote('hyper,176,20')] ).
cnf(185,plain,
( n4
| n5(s6) ),
inference(hyper,[status(thm)],[177,13]),
[iquote('hyper,177,13')] ).
cnf(191,plain,
( n4
| q(s6) ),
inference(hyper,[status(thm)],[185,15,178]),
[iquote('hyper,185,15,178')] ).
cnf(192,plain,
( n4
| q(A) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[191,16,185])]),
[iquote('hyper,191,16,185,factor_simp')] ).
cnf(195,plain,
( n4
| n8 ),
inference(hyper,[status(thm)],[192,8]),
[iquote('hyper,192,8')] ).
cnf(196,plain,
( n4
| n7 ),
inference(hyper,[status(thm)],[195,31,137]),
[iquote('hyper,195,31,137')] ).
cnf(197,plain,
( n4
| p(s7) ),
inference(hyper,[status(thm)],[196,11]),
[iquote('hyper,196,11')] ).
cnf(199,plain,
( n4
| p(s2) ),
inference(hyper,[status(thm)],[197,25,157]),
[iquote('hyper,197,25,157')] ).
cnf(204,plain,
( n4
| p(A) ),
inference(hyper,[status(thm)],[199,24,157]),
[iquote('hyper,199,24,157')] ).
cnf(206,plain,
n4,
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[204,17])]),
[iquote('hyper,204,17,factor_simp')] ).
cnf(207,plain,
n9,
inference(hyper,[status(thm)],[206,26,176]),
[iquote('hyper,206,26,176')] ).
cnf(208,plain,
p(A),
inference(hyper,[status(thm)],[206,18]),
[iquote('hyper,206,18')] ).
cnf(217,plain,
n7,
inference(hyper,[status(thm)],[208,10]),
[iquote('hyper,208,10')] ).
cnf(218,plain,
n8,
inference(hyper,[status(thm)],[217,30,137]),
[iquote('hyper,217,30,137')] ).
cnf(219,plain,
q(A),
inference(hyper,[status(thm)],[218,9]),
[iquote('hyper,218,9')] ).
cnf(220,plain,
n5(A),
inference(hyper,[status(thm)],[219,14,219]),
[iquote('hyper,219,14,219')] ).
cnf(221,plain,
n6,
inference(hyper,[status(thm)],[220,12]),
[iquote('hyper,220,12')] ).
cnf(222,plain,
$false,
inference(hyper,[status(thm)],[221,1,156,207,137]),
[iquote('hyper,221,1,156,207,137')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SYN037-1 : TPTP v8.1.0. Released v1.0.0.
% 0.06/0.12 % Command : otter-tptp-script %s
% 0.12/0.33 % Computer : n014.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:15:24 EDT 2022
% 0.12/0.33 % CPUTime :
% 1.87/2.05 ----- Otter 3.3f, August 2004 -----
% 1.87/2.05 The process was started by sandbox2 on n014.cluster.edu,
% 1.87/2.05 Wed Jul 27 11:15:24 2022
% 1.87/2.05 The command was "./otter". The process ID is 28161.
% 1.87/2.05
% 1.87/2.05 set(prolog_style_variables).
% 1.87/2.05 set(auto).
% 1.87/2.05 dependent: set(auto1).
% 1.87/2.05 dependent: set(process_input).
% 1.87/2.05 dependent: clear(print_kept).
% 1.87/2.05 dependent: clear(print_new_demod).
% 1.87/2.05 dependent: clear(print_back_demod).
% 1.87/2.05 dependent: clear(print_back_sub).
% 1.87/2.05 dependent: set(control_memory).
% 1.87/2.05 dependent: assign(max_mem, 12000).
% 1.87/2.05 dependent: assign(pick_given_ratio, 4).
% 1.87/2.05 dependent: assign(stats_level, 1).
% 1.87/2.05 dependent: assign(max_seconds, 10800).
% 1.87/2.05 clear(print_given).
% 1.87/2.05
% 1.87/2.05 list(usable).
% 1.87/2.05 0 [] -n2| -n9| -n6| -n10.
% 1.87/2.05 0 [] -n2| -n9|n6|n10.
% 1.87/2.05 0 [] n2|n9| -n6| -n10.
% 1.87/2.05 0 [] n2|n9|n6|n10.
% 1.87/2.05 0 [] -n2|n9| -n6|n10.
% 1.87/2.05 0 [] -n2|n9|n6| -n10.
% 1.87/2.05 0 [] n2| -n9| -n6|n10.
% 1.87/2.05 0 [] n2| -n9|n6| -n10.
% 1.87/2.05 0 [] -q(s8)|n8.
% 1.87/2.05 0 [] -n8|q(X10).
% 1.87/2.05 0 [] -p(X9)|n7.
% 1.87/2.05 0 [] -n7|p(s7).
% 1.87/2.05 0 [] -n5(X8)|n6.
% 1.87/2.05 0 [] -n6|n5(s6).
% 1.87/2.05 0 [] -q(s5(W))| -q(W)|n5(W).
% 1.87/2.05 0 [] q(s5(W))|q(W)|n5(W).
% 1.87/2.05 0 [] -n5(W)| -q(X7)|q(W).
% 1.87/2.05 0 [] -n5(W)|q(X7)| -q(W).
% 1.87/2.05 0 [] -p(s4)|n4.
% 1.87/2.05 0 [] -n4|p(X6).
% 1.87/2.05 0 [] -q(X5)|n3.
% 1.87/2.05 0 [] -n3|q(s3).
% 1.87/2.05 0 [] -n1(X4)|n2.
% 1.87/2.05 0 [] -n2|n1(s2).
% 1.87/2.05 0 [] -p(X)| -p(s1(X))|n1(X).
% 1.87/2.05 0 [] p(X)|p(s1(X))|n1(X).
% 1.87/2.05 0 [] -n1(X)| -p(X)|p(X3).
% 1.87/2.05 0 [] -n1(X)|p(X)| -p(X3).
% 1.87/2.05 0 [] -n3| -n4|n9.
% 1.87/2.05 0 [] n3|n4|n9.
% 1.87/2.05 0 [] -n3|n4| -n9.
% 1.87/2.05 0 [] n3| -n4| -n9.
% 1.87/2.05 0 [] -n7| -n8|n10.
% 1.87/2.05 0 [] n7|n8|n10.
% 1.87/2.05 0 [] -n7|n8| -n10.
% 1.87/2.05 0 [] n7| -n8| -n10.
% 1.87/2.05 end_of_list.
% 1.87/2.05
% 1.87/2.05 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=4.
% 1.87/2.05
% 1.87/2.05 This is a non-Horn set without equality. The strategy will
% 1.87/2.05 be ordered hyper_res, unit deletion, and factoring, with
% 1.87/2.05 satellites in sos and with nuclei in usable.
% 1.87/2.05
% 1.87/2.05 dependent: set(hyper_res).
% 1.87/2.05 dependent: set(factor).
% 1.87/2.05 dependent: set(unit_deletion).
% 1.87/2.05
% 1.87/2.05 ------------> process usable:
% 1.87/2.05 ** KEPT (pick-wt=4): 1 [] -n2| -n9| -n6| -n10.
% 1.87/2.05 ** KEPT (pick-wt=4): 2 [] -n2| -n9|n6|n10.
% 1.87/2.05 ** KEPT (pick-wt=4): 3 [] n2|n9| -n6| -n10.
% 1.87/2.05 ** KEPT (pick-wt=4): 4 [] -n2|n9| -n6|n10.
% 1.87/2.05 ** KEPT (pick-wt=4): 5 [] -n2|n9|n6| -n10.
% 1.87/2.05 ** KEPT (pick-wt=4): 6 [] n2| -n9| -n6|n10.
% 1.87/2.05 ** KEPT (pick-wt=4): 7 [] n2| -n9|n6| -n10.
% 1.87/2.05 ** KEPT (pick-wt=3): 8 [] -q(s8)|n8.
% 1.87/2.05 ** KEPT (pick-wt=3): 9 [] -n8|q(A).
% 1.87/2.05 ** KEPT (pick-wt=3): 10 [] -p(A)|n7.
% 1.87/2.05 ** KEPT (pick-wt=3): 11 [] -n7|p(s7).
% 1.87/2.05 ** KEPT (pick-wt=3): 12 [] -n5(A)|n6.
% 1.87/2.05 ** KEPT (pick-wt=3): 13 [] -n6|n5(s6).
% 1.87/2.05 ** KEPT (pick-wt=7): 14 [] -q(s5(A))| -q(A)|n5(A).
% 1.87/2.05 ** KEPT (pick-wt=6): 15 [] -n5(A)| -q(B)|q(A).
% 1.87/2.05 ** KEPT (pick-wt=6): 16 [] -n5(A)|q(B)| -q(A).
% 1.87/2.05 ** KEPT (pick-wt=3): 17 [] -p(s4)|n4.
% 1.87/2.05 ** KEPT (pick-wt=3): 18 [] -n4|p(A).
% 1.87/2.05 ** KEPT (pick-wt=3): 19 [] -q(A)|n3.
% 1.87/2.05 ** KEPT (pick-wt=3): 20 [] -n3|q(s3).
% 1.87/2.05 ** KEPT (pick-wt=3): 21 [] -n1(A)|n2.
% 1.87/2.05 ** KEPT (pick-wt=3): 22 [] -n2|n1(s2).
% 1.87/2.05 ** KEPT (pick-wt=7): 23 [] -p(A)| -p(s1(A))|n1(A).
% 1.87/2.05 ** KEPT (pick-wt=6): 24 [] -n1(A)| -p(A)|p(B).
% 1.87/2.05 ** KEPT (pick-wt=6): 25 [] -n1(A)|p(A)| -p(B).
% 1.87/2.05 ** KEPT (pick-wt=3): 26 [] -n3| -n4|n9.
% 1.87/2.05 ** KEPT (pick-wt=3): 27 [] -n3|n4| -n9.
% 1.87/2.05 ** KEPT (pick-wt=3): 28 [] n3| -n4| -n9.
% 1.87/2.05 ** KEPT (pick-wt=3): 29 [] -n7| -n8|n10.
% 1.87/2.05 ** KEPT (pick-wt=3): 30 [] -n7|n8| -n10.
% 1.87/2.05 ** KEPT (pick-wt=3): 31 [] n7| -n8| -n10.
% 1.87/2.05
% 1.87/2.05 ------------> process sos:
% 1.87/2.05 ** KEPT (pick-wt=4): 32 [] n2|n9|n6|n10.
% 1.87/2.05 ** KEPT (pick-wt=7): 33 [] q(s5(A))|q(A)|n5(A).
% 1.87/2.05 ** KEPT (pick-wt=7): 34 [] p(A)|p(s1(A))|n1(A).
% 1.87/2.05 ** KEPT (pick-wt=3): 35 [] n3|n4|n9.
% 1.87/2.05 ** KEPT (pick-wt=3): 36 [] n7|n8|n10.
% 1.87/2.05
% 1.87/2.05 ======= end of input processing =======
% 1.87/2.05
% 1.87/2.05 =========== start of search ===========
% 1.87/2.05
% 1.87/2.05 -------- PROOF --------
% 1.87/2.05
% 1.87/2.05 -----> EMPTY CLAUSE at 0.11 sec ----> 222 [hyper,221,1,156,207,137] $F.
% 1.87/2.05
% 1.87/2.05 Length of proof is 83. Level of proof is 60.
% 1.87/2.05
% 1.87/2.05 ---------------- PROOF ----------------
% 1.87/2.05 % SZS status Unsatisfiable
% 1.87/2.05 % SZS output start Refutation
% See solution above
% 1.87/2.05 ------------ end of proof -------------
% 1.87/2.05
% 1.87/2.05
% 1.87/2.05 Search stopped by max_proofs option.
% 1.87/2.05
% 1.87/2.05
% 1.87/2.05 Search stopped by max_proofs option.
% 1.87/2.05
% 1.87/2.05 ============ end of search ============
% 1.87/2.05
% 1.87/2.05 -------------- statistics -------------
% 1.87/2.05 clauses given 114
% 1.87/2.05 clauses generated 1361
% 1.87/2.05 clauses kept 221
% 1.87/2.05 clauses forward subsumed 1175
% 1.87/2.05 clauses back subsumed 208
% 1.87/2.05 Kbytes malloced 976
% 1.87/2.05
% 1.87/2.05 ----------- times (seconds) -----------
% 1.87/2.05 user CPU time 0.12 (0 hr, 0 min, 0 sec)
% 1.87/2.05 system CPU time 0.00 (0 hr, 0 min, 0 sec)
% 1.87/2.05 wall-clock time 1 (0 hr, 0 min, 1 sec)
% 1.87/2.05
% 1.87/2.05 That finishes the proof of the theorem.
% 1.87/2.05
% 1.87/2.05 Process 28161 finished Wed Jul 27 11:15:25 2022
% 1.87/2.05 Otter interrupted
% 1.87/2.05 PROOF FOUND
%------------------------------------------------------------------------------