%------------------------------------------------------------------------------
% File : Otter---3.3
% Problem : KRS103+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : otter-tptp-script %s
% Computer : n025.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:01:09 EDT 2022
% Result : Unsatisfiable 2.00s 2.20s
% Output : Refutation 2.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 28
% Syntax : Number of clauses : 76 ( 7 unt; 60 nHn; 76 RR)
% Number of literals : 211 ( 0 equ; 36 neg)
% Maximal clause size : 4 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 20 ( 19 usr; 1 prp; 0-1 aty)
% Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% Number of variables : 27 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(4,axiom,
( ~ cTest(A)
| cminus3(A)
| cminus5(A)
| cminus8(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(5,axiom,
( ~ cTest(A)
| cminus3(A)
| cplus7(A)
| cplus8(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(7,axiom,
( ~ cTest(A)
| cplus3(A)
| cminus7(A)
| cplus8(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(10,axiom,
( ~ cTest(A)
| cminus9(A)
| cminus4(A)
| cminus8(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(16,axiom,
( ~ cTest(A)
| cminus3(A)
| cplus5(A)
| cminus8(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(18,axiom,
( ~ cTest(A)
| cplus3(A)
| cplus4(A)
| cplus1(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(19,axiom,
( ~ cTest(A)
| cminus2(A)
| cplus6(A)
| cplus9(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(21,axiom,
( ~ cTest(A)
| cminus3(A)
| cplus2(A)
| cplus8(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(22,axiom,
( ~ cTest(A)
| cminus2(A)
| cplus4(A)
| cminus6(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(23,axiom,
( ~ cTest(A)
| cminus2(A)
| cplus6(A)
| cminus7(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(25,axiom,
( ~ cTest(A)
| cminus9(A)
| cminus2(A)
| cminus5(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(26,axiom,
( ~ cTest(A)
| cplus3(A)
| cplus4(A)
| cplus9(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(30,axiom,
( ~ cTest(A)
| cminus4(A)
| cminus3(A)
| cminus7(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(32,axiom,
( ~ cTest(A)
| cminus4(A)
| cminus8(A)
| cplus9(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(35,axiom,
( ~ cTest(A)
| cminus4(A)
| cplus9(A)
| cplus7(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(36,axiom,
( ~ cTest(A)
| cminus9(A)
| cminus2(A)
| cplus3(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(37,axiom,
( ~ cTest(A)
| cminus1(A)
| cplus4(A)
| cplus2(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(46,axiom,
( ~ cTest(A)
| cminus4(A)
| cplus2(A)
| cplus8(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(48,axiom,
( ~ cminus8(A)
| ~ cplus8(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(49,axiom,
( ~ cminus9(A)
| ~ cplus9(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(50,axiom,
( ~ cplus4(A)
| ~ cminus4(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(51,axiom,
( ~ cminus7(A)
| ~ cplus7(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(52,axiom,
( ~ cplus3(A)
| ~ cminus3(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(53,axiom,
( ~ cplus5(A)
| ~ cminus5(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(54,axiom,
( ~ cminus2(A)
| ~ cplus2(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(55,axiom,
( ~ cminus1(A)
| ~ cplus1(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(56,axiom,
( ~ cplus6(A)
| ~ cminus6(A) ),
file('KRS103+1.p',unknown),
[] ).
cnf(59,axiom,
cTest(i2003_11_14_17_20_46476),
file('KRS103+1.p',unknown),
[] ).
cnf(61,plain,
( cminus4(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[59,46]),
[iquote('hyper,59,46')] ).
cnf(70,plain,
( cminus1(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[59,37]),
[iquote('hyper,59,37')] ).
cnf(71,plain,
( cminus9(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[59,36]),
[iquote('hyper,59,36')] ).
cnf(72,plain,
( cminus4(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[59,35]),
[iquote('hyper,59,35')] ).
cnf(75,plain,
( cminus4(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[59,32]),
[iquote('hyper,59,32')] ).
cnf(77,plain,
( cminus4(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[59,30]),
[iquote('hyper,59,30')] ).
cnf(81,plain,
( cplus3(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[59,26]),
[iquote('hyper,59,26')] ).
cnf(82,plain,
( cminus9(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| cminus5(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[59,25]),
[iquote('hyper,59,25')] ).
cnf(84,plain,
( cminus2(i2003_11_14_17_20_46476)
| cplus6(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[59,23]),
[iquote('hyper,59,23')] ).
cnf(85,plain,
( cminus2(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476)
| cminus6(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[59,22]),
[iquote('hyper,59,22')] ).
cnf(86,plain,
( cminus3(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[59,21]),
[iquote('hyper,59,21')] ).
cnf(88,plain,
( cminus2(i2003_11_14_17_20_46476)
| cplus6(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[59,19]),
[iquote('hyper,59,19')] ).
cnf(89,plain,
( cplus3(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476)
| cplus1(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[59,18]),
[iquote('hyper,59,18')] ).
cnf(91,plain,
( cminus3(i2003_11_14_17_20_46476)
| cplus5(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[59,16]),
[iquote('hyper,59,16')] ).
cnf(97,plain,
( cminus9(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[59,10]),
[iquote('hyper,59,10')] ).
cnf(100,plain,
( cplus3(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[59,7]),
[iquote('hyper,59,7')] ).
cnf(102,plain,
( cminus3(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[59,5]),
[iquote('hyper,59,5')] ).
cnf(103,plain,
( cminus3(i2003_11_14_17_20_46476)
| cminus5(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[59,4]),
[iquote('hyper,59,4')] ).
cnf(112,plain,
( cminus2(i2003_11_14_17_20_46476)
| cplus6(i2003_11_14_17_20_46476)
| cminus5(i2003_11_14_17_20_46476) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[88,49,82])]),
[iquote('hyper,88,49,82,factor_simp')] ).
cnf(119,plain,
( cminus4(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[97,49,75])])]),
[iquote('hyper,97,49,75,factor_simp,factor_simp')] ).
cnf(121,plain,
( cminus4(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[119,48,61])]),
[iquote('hyper,119,48,61,factor_simp')] ).
cnf(125,plain,
( cplus3(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[100,48,119]),
[iquote('hyper,100,48,119')] ).
cnf(127,plain,
( cminus3(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[102,48,119]),
[iquote('hyper,102,48,119')] ).
cnf(130,plain,
( cminus3(i2003_11_14_17_20_46476)
| cminus5(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[103,48,86])]),
[iquote('hyper,103,48,86,factor_simp')] ).
cnf(133,plain,
( cminus3(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[127,51,77])])]),
[iquote('hyper,127,51,77,factor_simp,factor_simp')] ).
cnf(136,plain,
( cminus3(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| cminus6(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[133,50,85]),
[iquote('hyper,133,50,85')] ).
cnf(139,plain,
( cminus3(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| cminus5(i2003_11_14_17_20_46476) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[136,56,112])]),
[iquote('hyper,136,56,112,factor_simp')] ).
cnf(142,plain,
( cminus3(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[136,56,84])]),
[iquote('hyper,136,56,84,factor_simp')] ).
cnf(144,plain,
( cminus3(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[139,53,91])]),
[iquote('hyper,139,53,91,factor_simp')] ).
cnf(146,plain,
( cminus3(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[144,48,102])]),
[iquote('hyper,144,48,102,factor_simp')] ).
cnf(149,plain,
( cminus3(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[146,51,142])])]),
[iquote('hyper,146,51,142,factor_simp,factor_simp')] ).
cnf(150,plain,
( cminus2(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[149,52,125]),
[iquote('hyper,149,52,125')] ).
cnf(151,plain,
( cminus2(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[149,52,71])]),
[iquote('hyper,149,52,71,factor_simp')] ).
cnf(159,plain,
( cminus2(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[151,49,81]),
[iquote('hyper,151,49,81')] ).
cnf(161,plain,
( cminus2(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[151,49,72]),
[iquote('hyper,151,49,72')] ).
cnf(166,plain,
( cminus2(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[161,51,150])])]),
[iquote('hyper,161,51,150,factor_simp,factor_simp')] ).
cnf(168,plain,
( cminus2(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[166,50,159])]),
[iquote('hyper,166,50,159,factor_simp')] ).
cnf(172,plain,
cminus2(i2003_11_14_17_20_46476),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[168,52,149])]),
[iquote('hyper,168,52,149,factor_simp')] ).
cnf(174,plain,
( cminus3(i2003_11_14_17_20_46476)
| cminus5(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[172,54,130]),
[iquote('hyper,172,54,130')] ).
cnf(175,plain,
cminus4(i2003_11_14_17_20_46476),
inference(hyper,[status(thm)],[172,54,121]),
[iquote('hyper,172,54,121')] ).
cnf(179,plain,
( cplus3(i2003_11_14_17_20_46476)
| cplus1(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[175,50,89]),
[iquote('hyper,175,50,89')] ).
cnf(181,plain,
( cminus1(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476) ),
inference(hyper,[status(thm)],[175,50,70]),
[iquote('hyper,175,50,70')] ).
cnf(182,plain,
( cminus3(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[174,53,91])]),
[iquote('hyper,174,53,91,factor_simp')] ).
cnf(188,plain,
cminus1(i2003_11_14_17_20_46476),
inference(hyper,[status(thm)],[181,54,172]),
[iquote('hyper,181,54,172')] ).
cnf(192,plain,
( cminus3(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[182,48,86])]),
[iquote('hyper,182,48,86,factor_simp')] ).
cnf(197,plain,
cminus3(i2003_11_14_17_20_46476),
inference(hyper,[status(thm)],[192,54,172]),
[iquote('hyper,192,54,172')] ).
cnf(199,plain,
cplus1(i2003_11_14_17_20_46476),
inference(hyper,[status(thm)],[197,52,179]),
[iquote('hyper,197,52,179')] ).
cnf(203,plain,
$false,
inference(hyper,[status(thm)],[199,55,188]),
[iquote('hyper,199,55,188')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.11 % Problem : KRS103+1 : TPTP v8.1.0. Released v3.1.0.
% 0.07/0.12 % Command : otter-tptp-script %s
% 0.12/0.33 % Computer : n025.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 03:40:00 EDT 2022
% 0.12/0.33 % CPUTime :
% 2.00/2.20 ----- Otter 3.3f, August 2004 -----
% 2.00/2.20 The process was started by sandbox on n025.cluster.edu,
% 2.00/2.20 Wed Jul 27 03:40:00 2022
% 2.00/2.20 The command was "./otter". The process ID is 28788.
% 2.00/2.20
% 2.00/2.20 set(prolog_style_variables).
% 2.00/2.20 set(auto).
% 2.00/2.20 dependent: set(auto1).
% 2.00/2.20 dependent: set(process_input).
% 2.00/2.20 dependent: clear(print_kept).
% 2.00/2.20 dependent: clear(print_new_demod).
% 2.00/2.20 dependent: clear(print_back_demod).
% 2.00/2.20 dependent: clear(print_back_sub).
% 2.00/2.20 dependent: set(control_memory).
% 2.00/2.20 dependent: assign(max_mem, 12000).
% 2.00/2.20 dependent: assign(pick_given_ratio, 4).
% 2.00/2.20 dependent: assign(stats_level, 1).
% 2.00/2.20 dependent: assign(max_seconds, 10800).
% 2.00/2.20 clear(print_given).
% 2.00/2.20
% 2.00/2.20 formula_list(usable).
% 2.00/2.20 all X (cowlThing(X)& -cowlNothing(X)).
% 2.00/2.20 all X (xsd_string(X)<-> -xsd_integer(X)).
% 2.00/2.20 all X (cTest(X)->cplus1(X)|cplus9(X)|cminus6(X)).
% 2.00/2.20 all X (cTest(X)->cminus3(X)|cminus5(X)|cminus8(X)).
% 2.00/2.20 all X (cTest(X)->cminus3(X)|cplus7(X)|cplus8(X)).
% 2.00/2.20 all X (cTest(X)->cminus4(X)|cplus6(X)|cplus8(X)).
% 2.00/2.20 all X (cTest(X)->cplus3(X)|cminus7(X)|cplus8(X)).
% 2.00/2.20 all X (cTest(X)->cminus4(X)|cplus5(X)|cplus9(X)).
% 2.00/2.20 all X (cTest(X)->cminus7(X)|cplus9(X)|cminus6(X)).
% 2.00/2.20 all X (cTest(X)->cminus9(X)|cminus4(X)|cminus8(X)).
% 2.00/2.20 all X (cTest(X)->cplus3(X)|cminus4(X)|cplus6(X)).
% 2.00/2.20 all X (cTest(X)->cplus4(X)|cplus6(X)|cminus8(X)).
% 2.00/2.20 all X (cTest(X)->cminus1(X)|cminus4(X)|cplus6(X)).
% 2.00/2.20 all X (cTest(X)->cplus2(X)|cplus5(X)|cplus9(X)).
% 2.00/2.20 all X (cTest(X)->cminus4(X)|cplus2(X)|cplus1(X)).
% 2.00/2.20 all X (cTest(X)->cminus3(X)|cplus5(X)|cminus8(X)).
% 2.00/2.20 all X (cTest(X)->cplus6(X)|cminus8(X)|cminus7(X)).
% 2.00/2.20 all X (cTest(X)->cplus3(X)|cplus4(X)|cplus1(X)).
% 2.00/2.20 all X (cTest(X)->cminus2(X)|cplus6(X)|cplus9(X)).
% 2.00/2.20 all X (cTest(X)->cplus2(X)|cplus1(X)|cminus6(X)).
% 2.00/2.20 all X (cTest(X)->cminus3(X)|cplus2(X)|cplus8(X)).
% 2.00/2.20 all X (cTest(X)->cminus2(X)|cplus4(X)|cminus6(X)).
% 2.00/2.20 all X (cTest(X)->cminus2(X)|cplus6(X)|cminus7(X)).
% 2.00/2.20 all X (cTest(X)->cplus5(X)|cminus7(X)|cplus9(X)).
% 2.00/2.20 all X (cTest(X)->cminus9(X)|cminus2(X)|cminus5(X)).
% 2.00/2.20 all X (cTest(X)->cplus3(X)|cplus4(X)|cplus9(X)).
% 2.00/2.20 all X (cTest(X)->cplus2(X)|cminus5(X)|cminus7(X)).
% 2.00/2.20 all X (cTest(X)->cplus4(X)|cminus5(X)|cplus6(X)).
% 2.00/2.20 all X (cTest(X)->cminus9(X)|cplus3(X)|cplus4(X)).
% 2.00/2.20 all X (cTest(X)->cminus4(X)|cminus3(X)|cminus7(X)).
% 2.00/2.20 all X (cTest(X)->cminus4(X)|cplus1(X)|cplus9(X)).
% 2.00/2.20 all X (cTest(X)->cminus4(X)|cminus8(X)|cplus9(X)).
% 2.00/2.20 all X (cTest(X)->cplus3(X)|cminus8(X)|cplus9(X)).
% 2.00/2.20 all X (cTest(X)->cminus9(X)|cminus2(X)|cplus7(X)).
% 2.00/2.20 all X (cTest(X)->cminus4(X)|cplus9(X)|cplus7(X)).
% 2.00/2.20 all X (cTest(X)->cminus9(X)|cminus2(X)|cplus3(X)).
% 2.00/2.20 all X (cTest(X)->cminus1(X)|cplus4(X)|cplus2(X)).
% 2.00/2.20 all X (cTest(X)->cminus2(X)|cminus3(X)|cplus1(X)).
% 2.00/2.20 all X (cTest(X)->cplus3(X)|cplus4(X)|cplus6(X)).
% 2.00/2.20 all X (cTest(X)->cminus2(X)|cplus3(X)|cminus8(X)).
% 2.00/2.20 all X (cTest(X)->cminus9(X)|cplus3(X)|cminus5(X)).
% 2.00/2.20 all X (cTest(X)->cplus4(X)|cplus1(X)|cplus7(X)).
% 2.00/2.20 all X (cTest(X)->cminus4(X)|cminus3(X)|cplus6(X)).
% 2.00/2.20 all X (cTest(X)->cminus9(X)|cplus1(X)|cminus6(X)).
% 2.00/2.20 all X (cTest(X)->cminus4(X)|cplus1(X)|cminus6(X)).
% 2.00/2.20 all X (cTest(X)->cminus4(X)|cplus2(X)|cplus8(X)).
% 2.00/2.20 all X (cTest(X)->cminus5(X)|cplus7(X)|cplus8(X)).
% 2.00/2.20 cTest(i2003_11_14_17_20_46476).
% 2.00/2.20 all X (-(cminus8(X)&cplus8(X))).
% 2.00/2.20 all X (-(cminus9(X)&cplus9(X))).
% 2.00/2.20 all X (-(cplus4(X)&cminus4(X))).
% 2.00/2.20 all X (-(cminus7(X)&cplus7(X))).
% 2.00/2.20 all X (-(cplus3(X)&cminus3(X))).
% 2.00/2.20 all X (-(cplus5(X)&cminus5(X))).
% 2.00/2.20 all X (-(cminus2(X)&cplus2(X))).
% 2.00/2.20 all X (-(cminus1(X)&cplus1(X))).
% 2.00/2.20 all X (-(cplus6(X)&cminus6(X))).
% 2.00/2.20 end_of_list.
% 2.00/2.20
% 2.00/2.20 -------> usable clausifies to:
% 2.00/2.20
% 2.00/2.20 list(usable).
% 2.00/2.20 0 [] cowlThing(X).
% 2.00/2.20 0 [] -cowlNothing(X).
% 2.00/2.20 0 [] -xsd_string(X)| -xsd_integer(X).
% 2.00/2.20 0 [] xsd_string(X)|xsd_integer(X).
% 2.00/2.20 0 [] -cTest(X)|cplus1(X)|cplus9(X)|cminus6(X).
% 2.00/2.20 0 [] -cTest(X)|cminus3(X)|cminus5(X)|cminus8(X).
% 2.00/2.20 0 [] -cTest(X)|cminus3(X)|cplus7(X)|cplus8(X).
% 2.00/2.20 0 [] -cTest(X)|cminus4(X)|cplus6(X)|cplus8(X).
% 2.00/2.20 0 [] -cTest(X)|cplus3(X)|cminus7(X)|cplus8(X).
% 2.00/2.20 0 [] -cTest(X)|cminus4(X)|cplus5(X)|cplus9(X).
% 2.00/2.20 0 [] -cTest(X)|cminus7(X)|cplus9(X)|cminus6(X).
% 2.00/2.20 0 [] -cTest(X)|cminus9(X)|cminus4(X)|cminus8(X).
% 2.00/2.20 0 [] -cTest(X)|cplus3(X)|cminus4(X)|cplus6(X).
% 2.00/2.20 0 [] -cTest(X)|cplus4(X)|cplus6(X)|cminus8(X).
% 2.00/2.20 0 [] -cTest(X)|cminus1(X)|cminus4(X)|cplus6(X).
% 2.00/2.20 0 [] -cTest(X)|cplus2(X)|cplus5(X)|cplus9(X).
% 2.00/2.20 0 [] -cTest(X)|cminus4(X)|cplus2(X)|cplus1(X).
% 2.00/2.20 0 [] -cTest(X)|cminus3(X)|cplus5(X)|cminus8(X).
% 2.00/2.20 0 [] -cTest(X)|cplus6(X)|cminus8(X)|cminus7(X).
% 2.00/2.20 0 [] -cTest(X)|cplus3(X)|cplus4(X)|cplus1(X).
% 2.00/2.20 0 [] -cTest(X)|cminus2(X)|cplus6(X)|cplus9(X).
% 2.00/2.20 0 [] -cTest(X)|cplus2(X)|cplus1(X)|cminus6(X).
% 2.00/2.20 0 [] -cTest(X)|cminus3(X)|cplus2(X)|cplus8(X).
% 2.00/2.20 0 [] -cTest(X)|cminus2(X)|cplus4(X)|cminus6(X).
% 2.00/2.20 0 [] -cTest(X)|cminus2(X)|cplus6(X)|cminus7(X).
% 2.00/2.20 0 [] -cTest(X)|cplus5(X)|cminus7(X)|cplus9(X).
% 2.00/2.20 0 [] -cTest(X)|cminus9(X)|cminus2(X)|cminus5(X).
% 2.00/2.20 0 [] -cTest(X)|cplus3(X)|cplus4(X)|cplus9(X).
% 2.00/2.20 0 [] -cTest(X)|cplus2(X)|cminus5(X)|cminus7(X).
% 2.00/2.20 0 [] -cTest(X)|cplus4(X)|cminus5(X)|cplus6(X).
% 2.00/2.20 0 [] -cTest(X)|cminus9(X)|cplus3(X)|cplus4(X).
% 2.00/2.20 0 [] -cTest(X)|cminus4(X)|cminus3(X)|cminus7(X).
% 2.00/2.20 0 [] -cTest(X)|cminus4(X)|cplus1(X)|cplus9(X).
% 2.00/2.20 0 [] -cTest(X)|cminus4(X)|cminus8(X)|cplus9(X).
% 2.00/2.20 0 [] -cTest(X)|cplus3(X)|cminus8(X)|cplus9(X).
% 2.00/2.20 0 [] -cTest(X)|cminus9(X)|cminus2(X)|cplus7(X).
% 2.00/2.20 0 [] -cTest(X)|cminus4(X)|cplus9(X)|cplus7(X).
% 2.00/2.20 0 [] -cTest(X)|cminus9(X)|cminus2(X)|cplus3(X).
% 2.00/2.20 0 [] -cTest(X)|cminus1(X)|cplus4(X)|cplus2(X).
% 2.00/2.20 0 [] -cTest(X)|cminus2(X)|cminus3(X)|cplus1(X).
% 2.00/2.20 0 [] -cTest(X)|cplus3(X)|cplus4(X)|cplus6(X).
% 2.00/2.20 0 [] -cTest(X)|cminus2(X)|cplus3(X)|cminus8(X).
% 2.00/2.20 0 [] -cTest(X)|cminus9(X)|cplus3(X)|cminus5(X).
% 2.00/2.20 0 [] -cTest(X)|cplus4(X)|cplus1(X)|cplus7(X).
% 2.00/2.20 0 [] -cTest(X)|cminus4(X)|cminus3(X)|cplus6(X).
% 2.00/2.20 0 [] -cTest(X)|cminus9(X)|cplus1(X)|cminus6(X).
% 2.00/2.20 0 [] -cTest(X)|cminus4(X)|cplus1(X)|cminus6(X).
% 2.00/2.20 0 [] -cTest(X)|cminus4(X)|cplus2(X)|cplus8(X).
% 2.00/2.20 0 [] -cTest(X)|cminus5(X)|cplus7(X)|cplus8(X).
% 2.00/2.20 0 [] cTest(i2003_11_14_17_20_46476).
% 2.00/2.20 0 [] -cminus8(X)| -cplus8(X).
% 2.00/2.20 0 [] -cminus9(X)| -cplus9(X).
% 2.00/2.20 0 [] -cplus4(X)| -cminus4(X).
% 2.00/2.20 0 [] -cminus7(X)| -cplus7(X).
% 2.00/2.20 0 [] -cplus3(X)| -cminus3(X).
% 2.00/2.20 0 [] -cplus5(X)| -cminus5(X).
% 2.00/2.20 0 [] -cminus2(X)| -cplus2(X).
% 2.00/2.20 0 [] -cminus1(X)| -cplus1(X).
% 2.00/2.20 0 [] -cplus6(X)| -cminus6(X).
% 2.00/2.20 end_of_list.
% 2.00/2.20
% 2.00/2.20 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=4.
% 2.00/2.20
% 2.00/2.20 This is a non-Horn set without equality. The strategy will
% 2.00/2.20 be ordered hyper_res, unit deletion, and factoring, with
% 2.00/2.20 satellites in sos and with nuclei in usable.
% 2.00/2.20
% 2.00/2.20 dependent: set(hyper_res).
% 2.00/2.20 dependent: set(factor).
% 2.00/2.20 dependent: set(unit_deletion).
% 2.00/2.20
% 2.00/2.20 ------------> process usable:
% 2.00/2.20 ** KEPT (pick-wt=2): 1 [] -cowlNothing(A).
% 2.00/2.20 ** KEPT (pick-wt=4): 2 [] -xsd_string(A)| -xsd_integer(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 3 [] -cTest(A)|cplus1(A)|cplus9(A)|cminus6(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 4 [] -cTest(A)|cminus3(A)|cminus5(A)|cminus8(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 5 [] -cTest(A)|cminus3(A)|cplus7(A)|cplus8(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 6 [] -cTest(A)|cminus4(A)|cplus6(A)|cplus8(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 7 [] -cTest(A)|cplus3(A)|cminus7(A)|cplus8(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 8 [] -cTest(A)|cminus4(A)|cplus5(A)|cplus9(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 9 [] -cTest(A)|cminus7(A)|cplus9(A)|cminus6(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 10 [] -cTest(A)|cminus9(A)|cminus4(A)|cminus8(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 11 [] -cTest(A)|cplus3(A)|cminus4(A)|cplus6(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 12 [] -cTest(A)|cplus4(A)|cplus6(A)|cminus8(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 13 [] -cTest(A)|cminus1(A)|cminus4(A)|cplus6(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 14 [] -cTest(A)|cplus2(A)|cplus5(A)|cplus9(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 15 [] -cTest(A)|cminus4(A)|cplus2(A)|cplus1(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 16 [] -cTest(A)|cminus3(A)|cplus5(A)|cminus8(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 17 [] -cTest(A)|cplus6(A)|cminus8(A)|cminus7(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 18 [] -cTest(A)|cplus3(A)|cplus4(A)|cplus1(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 19 [] -cTest(A)|cminus2(A)|cplus6(A)|cplus9(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 20 [] -cTest(A)|cplus2(A)|cplus1(A)|cminus6(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 21 [] -cTest(A)|cminus3(A)|cplus2(A)|cplus8(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 22 [] -cTest(A)|cminus2(A)|cplus4(A)|cminus6(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 23 [] -cTest(A)|cminus2(A)|cplus6(A)|cminus7(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 24 [] -cTest(A)|cplus5(A)|cminus7(A)|cplus9(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 25 [] -cTest(A)|cminus9(A)|cminus2(A)|cminus5(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 26 [] -cTest(A)|cplus3(A)|cplus4(A)|cplus9(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 27 [] -cTest(A)|cplus2(A)|cminus5(A)|cminus7(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 28 [] -cTest(A)|cplus4(A)|cminus5(A)|cplus6(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 29 [] -cTest(A)|cminus9(A)|cplus3(A)|cplus4(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 30 [] -cTest(A)|cminus4(A)|cminus3(A)|cminus7(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 31 [] -cTest(A)|cminus4(A)|cplus1(A)|cplus9(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 32 [] -cTest(A)|cminus4(A)|cminus8(A)|cplus9(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 33 [] -cTest(A)|cplus3(A)|cminus8(A)|cplus9(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 34 [] -cTest(A)|cminus9(A)|cminus2(A)|cplus7(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 35 [] -cTest(A)|cminus4(A)|cplus9(A)|cplus7(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 36 [] -cTest(A)|cminus9(A)|cminus2(A)|cplus3(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 37 [] -cTest(A)|cminus1(A)|cplus4(A)|cplus2(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 38 [] -cTest(A)|cminus2(A)|cminus3(A)|cplus1(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 39 [] -cTest(A)|cplus3(A)|cplus4(A)|cplus6(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 40 [] -cTest(A)|cminus2(A)|cplus3(A)|cminus8(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 41 [] -cTest(A)|cminus9(A)|cplus3(A)|cminus5(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 42 [] -cTest(A)|cplus4(A)|cplus1(A)|cplus7(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 43 [] -cTest(A)|cminus4(A)|cminus3(A)|cplus6(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 44 [] -cTest(A)|cminus9(A)|cplus1(A)|cminus6(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 45 [] -cTest(A)|cminus4(A)|cplus1(A)|cminus6(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 46 [] -cTest(A)|cminus4(A)|cplus2(A)|cplus8(A).
% 2.00/2.20 ** KEPT (pick-wt=8): 47 [] -cTest(A)|cminus5(A)|cplus7(A)|cplus8(A).
% 2.00/2.20 ** KEPT (pick-wt=4): 48 [] -cminus8(A)| -cplus8(A).
% 2.00/2.20 ** KEPT (pick-wt=4): 49 [] -cminus9(A)| -cplus9(A).
% 2.00/2.20 ** KEPT (pick-wt=4): 50 [] -cplus4(A)| -cminus4(A).
% 2.00/2.20 ** KEPT (pick-wt=4): 51 [] -cminus7(A)| -cplus7(A).
% 2.00/2.20 ** KEPT (pick-wt=4): 52 [] -cplus3(A)| -cminus3(A).
% 2.00/2.20 ** KEPT (pick-wt=4): 53 [] -cplus5(A)| -cminus5(A).
% 2.00/2.20 ** KEPT (pick-wt=4): 54 [] -cminus2(A)| -cplus2(A).
% 2.00/2.20 ** KEPT (pick-wt=4): 55 [] -cminus1(A)| -cplus1(A).
% 2.00/2.20 ** KEPT (pick-wt=4): 56 [] -cplus6(A)| -cminus6(A).
% 2.00/2.20
% 2.00/2.20 ------------> process sos:
% 2.00/2.20 ** KEPT (pick-wt=2): 57 [] cowlThing(A).
% 2.00/2.20 ** KEPT (pick-wt=4): 58 [] xsd_string(A)|xsd_integer(A).
% 2.00/2.20 ** KEPT (pick-wt=2): 59 [] cTest(i2003_11_14_17_20_46476).
% 2.00/2.20
% 2.00/2.20 ======= end of input processing =======
% 2.00/2.20
% 2.00/2.20 =========== start of search ===========
% 2.00/2.20
% 2.00/2.20 -------- PROOF --------
% 2.00/2.20
% 2.00/2.20 -----> EMPTY CLAUSE at 0.01 sec ----> 203 [hyper,199,55,188] $F.
% 2.00/2.20
% 2.00/2.20 Length of proof is 47. Level of proof is 19.
% 2.00/2.20
% 2.00/2.20 ---------------- PROOF ----------------
% 2.00/2.20 % SZS status Theorem
% 2.00/2.20 % SZS output start Refutation
% See solution above
% 2.00/2.20 ------------ end of proof -------------
% 2.00/2.20
% 2.00/2.20
% 2.00/2.20 Search stopped by max_proofs option.
% 2.00/2.20
% 2.00/2.20
% 2.00/2.20 Search stopped by max_proofs option.
% 2.00/2.20
% 2.00/2.20 ============ end of search ============
% 2.00/2.20
% 2.00/2.20 -------------- statistics -------------
% 2.00/2.20 clauses given 108
% 2.00/2.20 clauses generated 189
% 2.00/2.20 clauses kept 202
% 2.00/2.20 clauses forward subsumed 45
% 2.00/2.20 clauses back subsumed 128
% 2.00/2.20 Kbytes malloced 976
% 2.00/2.20
% 2.00/2.20 ----------- times (seconds) -----------
% 2.00/2.20 user CPU time 0.01 (0 hr, 0 min, 0 sec)
% 2.00/2.20 system CPU time 0.00 (0 hr, 0 min, 0 sec)
% 2.00/2.20 wall-clock time 2 (0 hr, 0 min, 2 sec)
% 2.00/2.20
% 2.00/2.20 That finishes the proof of the theorem.
% 2.00/2.20
% 2.00/2.20 Process 28788 finished Wed Jul 27 03:40:02 2022
% 2.00/2.20 Otter interrupted
% 2.00/2.20 PROOF FOUND
%------------------------------------------------------------------------------