%------------------------------------------------------------------------------
% File : Otter---3.3
% Problem : KRS132+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : otter-tptp-script %s
% Computer : n021.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:13 EDT 2022
% Result : Theorem 1.67s 1.91s
% Output : Refutation 1.67s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
~ cowlNothing(A),
file('KRS132+1.p',unknown),
[] ).
cnf(2,axiom,
( ~ xsd_string(A)
| ~ xsd_integer(A) ),
file('KRS132+1.p',unknown),
[] ).
cnf(3,axiom,
( ~ cA(A)
| rq(A,dollar_f1(A)) ),
file('KRS132+1.p',unknown),
[] ).
cnf(5,axiom,
( cA(A)
| ~ rq(A,B)
| ~ cowlThing(B) ),
file('KRS132+1.p',unknown),
[] ).
cnf(6,axiom,
( ~ cAorB(A)
| rs(A,dollar_f2(A)) ),
file('KRS132+1.p',unknown),
[] ).
cnf(8,axiom,
( cAorB(A)
| ~ rs(A,B)
| ~ cowlThing(B) ),
file('KRS132+1.p',unknown),
[] ).
cnf(9,axiom,
( ~ cB(A)
| rr(A,dollar_f3(A)) ),
file('KRS132+1.p',unknown),
[] ).
cnf(11,axiom,
( cB(A)
| ~ rr(A,B)
| ~ cowlThing(B) ),
file('KRS132+1.p',unknown),
[] ).
cnf(12,axiom,
( ~ cNothing(A)
| rp(A,dollar_f4(A)) ),
file('KRS132+1.p',unknown),
[] ).
cnf(13,axiom,
( ~ cNothing(A)
| ~ rp(A,B) ),
file('KRS132+1.p',unknown),
[] ).
cnf(14,axiom,
( ~ cnotA(A)
| ~ rq(A,B)
| cNothing(B) ),
file('KRS132+1.p',unknown),
[] ).
cnf(16,axiom,
( ~ cnotAorB(A)
| ~ rs(A,B)
| cNothing(B) ),
file('KRS132+1.p',unknown),
[] ).
cnf(18,axiom,
( ~ cnotAorB(A)
| cnotB(A) ),
file('KRS132+1.p',unknown),
[] ).
cnf(19,axiom,
( ~ cnotAorB(A)
| cnotA(A) ),
file('KRS132+1.p',unknown),
[] ).
cnf(20,axiom,
( cnotAorB(A)
| ~ cnotB(A)
| ~ cnotA(A) ),
file('KRS132+1.p',unknown),
[] ).
cnf(21,axiom,
( ~ cnotB(A)
| ~ rr(A,B)
| cNothing(B) ),
file('KRS132+1.p',unknown),
[] ).
cnf(23,axiom,
( ~ cowlThing(dollar_c1)
| cowlNothing(dollar_c1)
| xsd_string(dollar_c2)
| ~ xsd_integer(dollar_c2)
| cAorB(dollar_c3)
| cB(dollar_c3)
| cA(dollar_c3) ),
file('KRS132+1.p',unknown),
[] ).
cnf(24,plain,
( ~ cowlThing(dollar_c1)
| xsd_string(dollar_c2)
| ~ xsd_integer(dollar_c2)
| cAorB(dollar_c3)
| cB(dollar_c3)
| cA(dollar_c3) ),
inference(unit_del,[status(thm)],[inference(copy,[status(thm)],[23]),1]),
[iquote('copy,23,unit_del,1')] ).
cnf(25,axiom,
( ~ cowlThing(dollar_c1)
| cowlNothing(dollar_c1)
| xsd_string(dollar_c2)
| ~ xsd_integer(dollar_c2)
| ~ cAorB(dollar_c3)
| ~ cB(dollar_c3) ),
file('KRS132+1.p',unknown),
[] ).
cnf(26,plain,
( ~ cowlThing(dollar_c1)
| xsd_string(dollar_c2)
| ~ xsd_integer(dollar_c2)
| ~ cAorB(dollar_c3)
| ~ cB(dollar_c3) ),
inference(unit_del,[status(thm)],[inference(copy,[status(thm)],[25]),1]),
[iquote('copy,25,unit_del,1')] ).
cnf(27,axiom,
( ~ cowlThing(dollar_c1)
| cowlNothing(dollar_c1)
| xsd_string(dollar_c2)
| ~ xsd_integer(dollar_c2)
| ~ cAorB(dollar_c3)
| ~ cA(dollar_c3) ),
file('KRS132+1.p',unknown),
[] ).
cnf(28,plain,
( ~ cowlThing(dollar_c1)
| xsd_string(dollar_c2)
| ~ xsd_integer(dollar_c2)
| ~ cAorB(dollar_c3)
| ~ cA(dollar_c3) ),
inference(unit_del,[status(thm)],[inference(copy,[status(thm)],[27]),1]),
[iquote('copy,27,unit_del,1')] ).
cnf(29,axiom,
( ~ cowlThing(dollar_c1)
| cowlNothing(dollar_c1)
| ~ xsd_string(dollar_c2)
| xsd_integer(dollar_c2)
| cAorB(dollar_c3)
| cB(dollar_c3)
| cA(dollar_c3) ),
file('KRS132+1.p',unknown),
[] ).
cnf(30,plain,
( ~ cowlThing(dollar_c1)
| ~ xsd_string(dollar_c2)
| xsd_integer(dollar_c2)
| cAorB(dollar_c3)
| cB(dollar_c3)
| cA(dollar_c3) ),
inference(unit_del,[status(thm)],[inference(copy,[status(thm)],[29]),1]),
[iquote('copy,29,unit_del,1')] ).
cnf(31,axiom,
( ~ cowlThing(dollar_c1)
| cowlNothing(dollar_c1)
| ~ xsd_string(dollar_c2)
| xsd_integer(dollar_c2)
| ~ cAorB(dollar_c3)
| ~ cB(dollar_c3) ),
file('KRS132+1.p',unknown),
[] ).
cnf(32,plain,
( ~ cowlThing(dollar_c1)
| ~ xsd_string(dollar_c2)
| xsd_integer(dollar_c2)
| ~ cAorB(dollar_c3)
| ~ cB(dollar_c3) ),
inference(unit_del,[status(thm)],[inference(copy,[status(thm)],[31]),1]),
[iquote('copy,31,unit_del,1')] ).
cnf(33,axiom,
( ~ cowlThing(dollar_c1)
| cowlNothing(dollar_c1)
| ~ xsd_string(dollar_c2)
| xsd_integer(dollar_c2)
| ~ cAorB(dollar_c3)
| ~ cA(dollar_c3) ),
file('KRS132+1.p',unknown),
[] ).
cnf(34,plain,
( ~ cowlThing(dollar_c1)
| ~ xsd_string(dollar_c2)
| xsd_integer(dollar_c2)
| ~ cAorB(dollar_c3)
| ~ cA(dollar_c3) ),
inference(unit_del,[status(thm)],[inference(copy,[status(thm)],[33]),1]),
[iquote('copy,33,unit_del,1')] ).
cnf(35,axiom,
cowlThing(A),
file('KRS132+1.p',unknown),
[] ).
cnf(36,axiom,
( xsd_string(A)
| xsd_integer(A) ),
file('KRS132+1.p',unknown),
[] ).
cnf(37,axiom,
( cnotA(A)
| rq(A,dollar_f5(A)) ),
file('KRS132+1.p',unknown),
[] ).
cnf(38,axiom,
( cnotAorB(A)
| rs(A,dollar_f6(A)) ),
file('KRS132+1.p',unknown),
[] ).
cnf(39,axiom,
( cnotB(A)
| rr(A,dollar_f7(A)) ),
file('KRS132+1.p',unknown),
[] ).
cnf(40,plain,
( xsd_integer(dollar_c2)
| cAorB(dollar_c3)
| cB(dollar_c3)
| cA(dollar_c3) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[36,30,35])]),
[iquote('hyper,36,30,35,factor_simp')] ).
cnf(41,plain,
( rs(A,dollar_f6(A))
| cnotA(A) ),
inference(hyper,[status(thm)],[38,19]),
[iquote('hyper,38,19')] ).
cnf(42,plain,
( rs(A,dollar_f6(A))
| cnotB(A) ),
inference(hyper,[status(thm)],[38,18]),
[iquote('hyper,38,18')] ).
cnf(43,plain,
( rr(A,dollar_f7(A))
| cnotAorB(A)
| rq(A,dollar_f5(A)) ),
inference(hyper,[status(thm)],[39,20,37]),
[iquote('hyper,39,20,37')] ).
cnf(44,plain,
( cAorB(dollar_c3)
| cB(dollar_c3)
| cA(dollar_c3)
| xsd_string(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[40,24,35])])])]),
[iquote('hyper,40,24,35,factor_simp,factor_simp,factor_simp')] ).
cnf(45,plain,
( cAorB(dollar_c3)
| cB(dollar_c3)
| cA(dollar_c3) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[44,2,40])])])]),
[iquote('hyper,44,2,40,factor_simp,factor_simp,factor_simp')] ).
cnf(46,plain,
( cAorB(dollar_c3)
| cA(dollar_c3)
| rr(dollar_c3,dollar_f3(dollar_c3)) ),
inference(hyper,[status(thm)],[45,9]),
[iquote('hyper,45,9')] ).
cnf(47,plain,
( cA(dollar_c3)
| rr(dollar_c3,dollar_f3(dollar_c3))
| rs(dollar_c3,dollar_f2(dollar_c3)) ),
inference(hyper,[status(thm)],[46,6]),
[iquote('hyper,46,6')] ).
cnf(48,plain,
( rr(dollar_c3,dollar_f3(dollar_c3))
| rs(dollar_c3,dollar_f2(dollar_c3))
| rq(dollar_c3,dollar_f1(dollar_c3)) ),
inference(hyper,[status(thm)],[47,3]),
[iquote('hyper,47,3')] ).
cnf(49,plain,
( rr(dollar_c3,dollar_f3(dollar_c3))
| rq(dollar_c3,dollar_f1(dollar_c3))
| cNothing(dollar_f2(dollar_c3))
| rr(dollar_c3,dollar_f7(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3)) ),
inference(hyper,[status(thm)],[48,16,43]),
[iquote('hyper,48,16,43')] ).
cnf(52,plain,
( rr(dollar_c3,dollar_f3(dollar_c3))
| rq(dollar_c3,dollar_f1(dollar_c3))
| rr(dollar_c3,dollar_f7(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3))) ),
inference(hyper,[status(thm)],[49,12]),
[iquote('hyper,49,12')] ).
cnf(57,plain,
( rr(dollar_c3,dollar_f3(dollar_c3))
| rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| cB(dollar_c3) ),
inference(hyper,[status(thm)],[52,11,35]),
[iquote('hyper,52,11,35')] ).
cnf(60,plain,
( rr(dollar_c3,dollar_f3(dollar_c3))
| rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3))) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[57,9])]),
[iquote('hyper,57,9,factor_simp')] ).
cnf(61,plain,
( rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| cNothing(dollar_f3(dollar_c3))
| rs(dollar_c3,dollar_f6(dollar_c3)) ),
inference(hyper,[status(thm)],[60,21,42]),
[iquote('hyper,60,21,42')] ).
cnf(62,plain,
( rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| cB(dollar_c3) ),
inference(hyper,[status(thm)],[60,11,35]),
[iquote('hyper,60,11,35')] ).
cnf(63,plain,
( rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rs(dollar_c3,dollar_f6(dollar_c3))
| rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3))) ),
inference(hyper,[status(thm)],[61,12]),
[iquote('hyper,61,12')] ).
cnf(64,plain,
( rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| cAorB(dollar_c3) ),
inference(hyper,[status(thm)],[63,8,35]),
[iquote('hyper,63,8,35')] ).
cnf(65,plain,
( rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| xsd_integer(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[64,32,35,36,62])])])])]),
[iquote('hyper,64,32,35,36,62,factor_simp,factor_simp,factor_simp,factor_simp')] ).
cnf(67,plain,
( rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| xsd_string(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[65,26,35,64,62])])])])])])])]),
[iquote('hyper,65,26,35,64,62,factor_simp,factor_simp,factor_simp,factor_simp,factor_simp,factor_simp,factor_simp')] ).
cnf(68,plain,
( rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3))) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[67,2,65])])])])]),
[iquote('hyper,67,2,65,factor_simp,factor_simp,factor_simp,factor_simp')] ).
cnf(73,plain,
( rq(dollar_c3,dollar_f1(dollar_c3))
| rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| cA(dollar_c3) ),
inference(hyper,[status(thm)],[68,5,35]),
[iquote('hyper,68,5,35')] ).
cnf(75,plain,
( rq(dollar_c3,dollar_f1(dollar_c3))
| rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3))) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[73,3])]),
[iquote('hyper,73,3,factor_simp')] ).
cnf(76,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| cNothing(dollar_f1(dollar_c3))
| rs(dollar_c3,dollar_f6(dollar_c3)) ),
inference(hyper,[status(thm)],[75,14,41]),
[iquote('hyper,75,14,41')] ).
cnf(77,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| cA(dollar_c3) ),
inference(hyper,[status(thm)],[75,5,35]),
[iquote('hyper,75,5,35')] ).
cnf(79,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rs(dollar_c3,dollar_f6(dollar_c3))
| rp(dollar_f1(dollar_c3),dollar_f4(dollar_f1(dollar_c3))) ),
inference(hyper,[status(thm)],[76,12]),
[iquote('hyper,76,12')] ).
cnf(80,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rp(dollar_f1(dollar_c3),dollar_f4(dollar_f1(dollar_c3)))
| cAorB(dollar_c3) ),
inference(hyper,[status(thm)],[79,8,35]),
[iquote('hyper,79,8,35')] ).
cnf(81,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rp(dollar_f1(dollar_c3),dollar_f4(dollar_f1(dollar_c3)))
| xsd_integer(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[80,34,35,36,77])])])]),
[iquote('hyper,80,34,35,36,77,factor_simp,factor_simp,factor_simp')] ).
cnf(83,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rp(dollar_f1(dollar_c3),dollar_f4(dollar_f1(dollar_c3)))
| xsd_string(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[81,28,35,80,77])])])])])]),
[iquote('hyper,81,28,35,80,77,factor_simp,factor_simp,factor_simp,factor_simp,factor_simp')] ).
cnf(84,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rp(dollar_f1(dollar_c3),dollar_f4(dollar_f1(dollar_c3))) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[83,2,81])])])]),
[iquote('hyper,83,2,81,factor_simp,factor_simp,factor_simp')] ).
cnf(89,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rs(dollar_c3,dollar_f6(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[84,13,76])])]),
[iquote('hyper,84,13,76,factor_simp,factor_simp')] ).
cnf(91,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| cAorB(dollar_c3) ),
inference(hyper,[status(thm)],[89,8,35]),
[iquote('hyper,89,8,35')] ).
cnf(92,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| xsd_integer(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[91,34,35,36,77])])])]),
[iquote('hyper,91,34,35,36,77,factor_simp,factor_simp,factor_simp')] ).
cnf(94,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| xsd_string(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[92,28,35,91,77])])])])]),
[iquote('hyper,92,28,35,91,77,factor_simp,factor_simp,factor_simp,factor_simp')] ).
cnf(95,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3))) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[94,2,92])])]),
[iquote('hyper,94,2,92,factor_simp,factor_simp')] ).
cnf(97,plain,
( rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rr(dollar_c3,dollar_f3(dollar_c3))
| rq(dollar_c3,dollar_f1(dollar_c3))
| rr(dollar_c3,dollar_f7(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3)) ),
inference(hyper,[status(thm)],[95,13,49]),
[iquote('hyper,95,13,49')] ).
cnf(98,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| rs(dollar_c3,dollar_f6(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[95,13,61])]),
[iquote('hyper,95,13,61,factor_simp')] ).
cnf(103,plain,
( rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rr(dollar_c3,dollar_f3(dollar_c3))
| rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| cB(dollar_c3) ),
inference(hyper,[status(thm)],[97,11,35]),
[iquote('hyper,97,11,35')] ).
cnf(104,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| cAorB(dollar_c3) ),
inference(hyper,[status(thm)],[98,8,35]),
[iquote('hyper,98,8,35')] ).
cnf(105,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| xsd_integer(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[104,32,35,36,62])])])])]),
[iquote('hyper,104,32,35,36,62,factor_simp,factor_simp,factor_simp,factor_simp')] ).
cnf(107,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| xsd_string(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[105,26,35,104,62])])])])])])]),
[iquote('hyper,105,26,35,104,62,factor_simp,factor_simp,factor_simp,factor_simp,factor_simp,factor_simp')] ).
cnf(108,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[107,2,105])])])]),
[iquote('hyper,107,2,105,factor_simp,factor_simp,factor_simp')] ).
cnf(114,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rq(dollar_c3,dollar_f1(dollar_c3))
| cA(dollar_c3) ),
inference(hyper,[status(thm)],[108,5,35]),
[iquote('hyper,108,5,35')] ).
cnf(116,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rq(dollar_c3,dollar_f1(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[114,3])]),
[iquote('hyper,114,3,factor_simp')] ).
cnf(117,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| cNothing(dollar_f1(dollar_c3))
| rs(dollar_c3,dollar_f6(dollar_c3)) ),
inference(hyper,[status(thm)],[116,14,41]),
[iquote('hyper,116,14,41')] ).
cnf(118,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| cA(dollar_c3) ),
inference(hyper,[status(thm)],[116,5,35]),
[iquote('hyper,116,5,35')] ).
cnf(120,plain,
( rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rr(dollar_c3,dollar_f3(dollar_c3))
| rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[103,9])]),
[iquote('hyper,103,9,factor_simp')] ).
cnf(122,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rs(dollar_c3,dollar_f6(dollar_c3))
| rp(dollar_f1(dollar_c3),dollar_f4(dollar_f1(dollar_c3))) ),
inference(hyper,[status(thm)],[117,12]),
[iquote('hyper,117,12')] ).
cnf(125,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rp(dollar_f1(dollar_c3),dollar_f4(dollar_f1(dollar_c3)))
| cAorB(dollar_c3) ),
inference(hyper,[status(thm)],[122,8,35]),
[iquote('hyper,122,8,35')] ).
cnf(126,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rp(dollar_f1(dollar_c3),dollar_f4(dollar_f1(dollar_c3)))
| xsd_integer(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[125,34,35,36,118])])]),
[iquote('hyper,125,34,35,36,118,factor_simp,factor_simp')] ).
cnf(128,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rp(dollar_f1(dollar_c3),dollar_f4(dollar_f1(dollar_c3)))
| xsd_string(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[126,28,35,125,118])])])]),
[iquote('hyper,126,28,35,125,118,factor_simp,factor_simp,factor_simp')] ).
cnf(129,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rp(dollar_f1(dollar_c3),dollar_f4(dollar_f1(dollar_c3))) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[128,2,126])])]),
[iquote('hyper,128,2,126,factor_simp,factor_simp')] ).
cnf(130,plain,
( rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| cNothing(dollar_f3(dollar_c3))
| rs(dollar_c3,dollar_f6(dollar_c3)) ),
inference(hyper,[status(thm)],[120,21,42]),
[iquote('hyper,120,21,42')] ).
cnf(133,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| rs(dollar_c3,dollar_f6(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[129,13,117])]),
[iquote('hyper,129,13,117,factor_simp')] ).
cnf(135,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| cAorB(dollar_c3) ),
inference(hyper,[status(thm)],[133,8,35]),
[iquote('hyper,133,8,35')] ).
cnf(136,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| xsd_integer(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[135,34,35,36,118])])]),
[iquote('hyper,135,34,35,36,118,factor_simp,factor_simp')] ).
cnf(138,plain,
( rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3)))
| xsd_string(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[136,28,35,135,118])])]),
[iquote('hyper,136,28,35,135,118,factor_simp,factor_simp')] ).
cnf(140,plain,
rp(dollar_f2(dollar_c3),dollar_f4(dollar_f2(dollar_c3))),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[138,2,136])]),
[iquote('hyper,138,2,136,factor_simp')] ).
cnf(142,plain,
( rr(dollar_c3,dollar_f3(dollar_c3))
| rq(dollar_c3,dollar_f1(dollar_c3))
| rr(dollar_c3,dollar_f7(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3)) ),
inference(hyper,[status(thm)],[140,13,49]),
[iquote('hyper,140,13,49')] ).
cnf(143,plain,
( rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| rs(dollar_c3,dollar_f6(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[130,12])]),
[iquote('hyper,130,12,factor_simp')] ).
cnf(147,plain,
( rr(dollar_c3,dollar_f3(dollar_c3))
| rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| cB(dollar_c3) ),
inference(hyper,[status(thm)],[142,11,35]),
[iquote('hyper,142,11,35')] ).
cnf(149,plain,
( rr(dollar_c3,dollar_f3(dollar_c3))
| rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[147,9])]),
[iquote('hyper,147,9,factor_simp')] ).
cnf(150,plain,
( rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| cNothing(dollar_f3(dollar_c3))
| rs(dollar_c3,dollar_f6(dollar_c3)) ),
inference(hyper,[status(thm)],[149,21,42]),
[iquote('hyper,149,21,42')] ).
cnf(151,plain,
( rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| cB(dollar_c3) ),
inference(hyper,[status(thm)],[149,11,35]),
[iquote('hyper,149,11,35')] ).
cnf(152,plain,
( rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| cAorB(dollar_c3) ),
inference(hyper,[status(thm)],[143,8,35]),
[iquote('hyper,143,8,35')] ).
cnf(153,plain,
( rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| xsd_integer(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[152,32,35,36,151])])])]),
[iquote('hyper,152,32,35,36,151,factor_simp,factor_simp,factor_simp')] ).
cnf(155,plain,
( rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| xsd_string(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[153,26,35,152,151])])])])])]),
[iquote('hyper,153,26,35,152,151,factor_simp,factor_simp,factor_simp,factor_simp,factor_simp')] ).
cnf(156,plain,
( rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[155,2,153])])])]),
[iquote('hyper,155,2,153,factor_simp,factor_simp,factor_simp')] ).
cnf(161,plain,
( rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rq(dollar_c3,dollar_f1(dollar_c3))
| cA(dollar_c3) ),
inference(hyper,[status(thm)],[156,5,35]),
[iquote('hyper,156,5,35')] ).
cnf(163,plain,
( rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rq(dollar_c3,dollar_f1(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[161,3])]),
[iquote('hyper,161,3,factor_simp')] ).
cnf(165,plain,
( rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| cNothing(dollar_f1(dollar_c3))
| rs(dollar_c3,dollar_f6(dollar_c3)) ),
inference(hyper,[status(thm)],[163,14,41]),
[iquote('hyper,163,14,41')] ).
cnf(166,plain,
( rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| cA(dollar_c3) ),
inference(hyper,[status(thm)],[163,5,35]),
[iquote('hyper,163,5,35')] ).
cnf(167,plain,
( rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rs(dollar_c3,dollar_f6(dollar_c3))
| rp(dollar_f1(dollar_c3),dollar_f4(dollar_f1(dollar_c3))) ),
inference(hyper,[status(thm)],[165,12]),
[iquote('hyper,165,12')] ).
cnf(168,plain,
( rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rp(dollar_f1(dollar_c3),dollar_f4(dollar_f1(dollar_c3)))
| cAorB(dollar_c3) ),
inference(hyper,[status(thm)],[167,8,35]),
[iquote('hyper,167,8,35')] ).
cnf(169,plain,
( rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rp(dollar_f1(dollar_c3),dollar_f4(dollar_f1(dollar_c3)))
| xsd_integer(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[168,34,35,36,166])])]),
[iquote('hyper,168,34,35,36,166,factor_simp,factor_simp')] ).
cnf(171,plain,
( rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rp(dollar_f1(dollar_c3),dollar_f4(dollar_f1(dollar_c3)))
| xsd_string(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[169,28,35,168,166])])])]),
[iquote('hyper,169,28,35,168,166,factor_simp,factor_simp,factor_simp')] ).
cnf(172,plain,
( rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rp(dollar_f1(dollar_c3),dollar_f4(dollar_f1(dollar_c3))) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[171,2,169])])]),
[iquote('hyper,171,2,169,factor_simp,factor_simp')] ).
cnf(175,plain,
( rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| rs(dollar_c3,dollar_f6(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[172,13,165])]),
[iquote('hyper,172,13,165,factor_simp')] ).
cnf(178,plain,
( rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| cAorB(dollar_c3) ),
inference(hyper,[status(thm)],[175,8,35]),
[iquote('hyper,175,8,35')] ).
cnf(179,plain,
( rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| xsd_integer(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[178,34,35,36,166])])]),
[iquote('hyper,178,34,35,36,166,factor_simp,factor_simp')] ).
cnf(181,plain,
( rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3)))
| xsd_string(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[179,28,35,178,166])])]),
[iquote('hyper,179,28,35,178,166,factor_simp,factor_simp')] ).
cnf(182,plain,
rp(dollar_f3(dollar_c3),dollar_f4(dollar_f3(dollar_c3))),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[181,2,179])]),
[iquote('hyper,181,2,179,factor_simp')] ).
cnf(183,plain,
( rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| rs(dollar_c3,dollar_f6(dollar_c3)) ),
inference(hyper,[status(thm)],[182,13,150]),
[iquote('hyper,182,13,150')] ).
cnf(185,plain,
( rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| cAorB(dollar_c3) ),
inference(hyper,[status(thm)],[183,8,35]),
[iquote('hyper,183,8,35')] ).
cnf(186,plain,
( rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| xsd_integer(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[185,32,35,36,151])])])]),
[iquote('hyper,185,32,35,36,151,factor_simp,factor_simp,factor_simp')] ).
cnf(188,plain,
( rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3))
| xsd_string(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[186,26,35,185,151])])])])]),
[iquote('hyper,186,26,35,185,151,factor_simp,factor_simp,factor_simp,factor_simp')] ).
cnf(189,plain,
( rq(dollar_c3,dollar_f1(dollar_c3))
| rq(dollar_c3,dollar_f5(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[188,2,186])])]),
[iquote('hyper,188,2,186,factor_simp,factor_simp')] ).
cnf(194,plain,
( rq(dollar_c3,dollar_f1(dollar_c3))
| cA(dollar_c3) ),
inference(hyper,[status(thm)],[189,5,35]),
[iquote('hyper,189,5,35')] ).
cnf(196,plain,
rq(dollar_c3,dollar_f1(dollar_c3)),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[194,3])]),
[iquote('hyper,194,3,factor_simp')] ).
cnf(198,plain,
( cNothing(dollar_f1(dollar_c3))
| rs(dollar_c3,dollar_f6(dollar_c3)) ),
inference(hyper,[status(thm)],[196,14,41]),
[iquote('hyper,196,14,41')] ).
cnf(199,plain,
cA(dollar_c3),
inference(hyper,[status(thm)],[196,5,35]),
[iquote('hyper,196,5,35')] ).
cnf(200,plain,
( rs(dollar_c3,dollar_f6(dollar_c3))
| rp(dollar_f1(dollar_c3),dollar_f4(dollar_f1(dollar_c3))) ),
inference(hyper,[status(thm)],[198,12]),
[iquote('hyper,198,12')] ).
cnf(201,plain,
( rp(dollar_f1(dollar_c3),dollar_f4(dollar_f1(dollar_c3)))
| cAorB(dollar_c3) ),
inference(hyper,[status(thm)],[200,8,35]),
[iquote('hyper,200,8,35')] ).
cnf(202,plain,
( rp(dollar_f1(dollar_c3),dollar_f4(dollar_f1(dollar_c3)))
| xsd_integer(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[201,34,35,36,199])]),
[iquote('hyper,201,34,35,36,199,factor_simp')] ).
cnf(204,plain,
( rp(dollar_f1(dollar_c3),dollar_f4(dollar_f1(dollar_c3)))
| xsd_string(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[202,28,35,201,199])]),
[iquote('hyper,202,28,35,201,199,factor_simp')] ).
cnf(205,plain,
rp(dollar_f1(dollar_c3),dollar_f4(dollar_f1(dollar_c3))),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[204,2,202])]),
[iquote('hyper,204,2,202,factor_simp')] ).
cnf(206,plain,
rs(dollar_c3,dollar_f6(dollar_c3)),
inference(hyper,[status(thm)],[205,13,198]),
[iquote('hyper,205,13,198')] ).
cnf(208,plain,
cAorB(dollar_c3),
inference(hyper,[status(thm)],[206,8,35]),
[iquote('hyper,206,8,35')] ).
cnf(209,plain,
xsd_integer(dollar_c2),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[208,34,35,36,199])]),
[iquote('hyper,208,34,35,36,199,factor_simp')] ).
cnf(211,plain,
xsd_string(dollar_c2),
inference(hyper,[status(thm)],[209,28,35,208,199]),
[iquote('hyper,209,28,35,208,199')] ).
cnf(212,plain,
$false,
inference(hyper,[status(thm)],[211,2,209]),
[iquote('hyper,211,2,209')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KRS132+1 : TPTP v8.1.0. Released v3.1.0.
% 0.07/0.12 % Command : otter-tptp-script %s
% 0.12/0.33 % Computer : n021.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:25:23 EDT 2022
% 0.12/0.33 % CPUTime :
% 1.67/1.90 ----- Otter 3.3f, August 2004 -----
% 1.67/1.90 The process was started by sandbox2 on n021.cluster.edu,
% 1.67/1.90 Wed Jul 27 03:25:23 2022
% 1.67/1.90 The command was "./otter". The process ID is 8787.
% 1.67/1.90
% 1.67/1.90 set(prolog_style_variables).
% 1.67/1.90 set(auto).
% 1.67/1.90 dependent: set(auto1).
% 1.67/1.90 dependent: set(process_input).
% 1.67/1.90 dependent: clear(print_kept).
% 1.67/1.90 dependent: clear(print_new_demod).
% 1.67/1.90 dependent: clear(print_back_demod).
% 1.67/1.90 dependent: clear(print_back_sub).
% 1.67/1.90 dependent: set(control_memory).
% 1.67/1.90 dependent: assign(max_mem, 12000).
% 1.67/1.90 dependent: assign(pick_given_ratio, 4).
% 1.67/1.90 dependent: assign(stats_level, 1).
% 1.67/1.90 dependent: assign(max_seconds, 10800).
% 1.67/1.90 clear(print_given).
% 1.67/1.90
% 1.67/1.90 formula_list(usable).
% 1.67/1.90 all X (cowlThing(X)& -cowlNothing(X)).
% 1.67/1.90 all X (xsd_string(X)<-> -xsd_integer(X)).
% 1.67/1.90 all X (cA(X)<-> (exists Y (rq(X,Y)&cowlThing(Y)))).
% 1.67/1.90 all X (cAorB(X)<-> (exists Y (rs(X,Y)&cowlThing(Y)))).
% 1.67/1.90 all X (cB(X)<-> (exists Y (rr(X,Y)&cowlThing(Y)))).
% 1.67/1.90 all X (cNothing(X)-> (exists Y0 rp(X,Y0))).
% 1.67/1.90 all X (cNothing(X)-> -(exists Y rp(X,Y))).
% 1.67/1.90 all X (cnotA(X)<-> (all Y (rq(X,Y)->cNothing(Y)))).
% 1.67/1.90 all X (cnotAorB(X)<-> (all Y (rs(X,Y)->cNothing(Y)))).
% 1.67/1.90 all X (cnotAorB(X)<->cnotB(X)&cnotA(X)).
% 1.67/1.90 all X (cnotB(X)<-> (all Y (rr(X,Y)->cNothing(Y)))).
% 1.67/1.90 -((all X (cowlThing(X)& -cowlNothing(X)))& (all X (xsd_string(X)<-> -xsd_integer(X)))& (all X (cAorB(X)<->cB(X)|cA(X)))).
% 1.67/1.90 end_of_list.
% 1.67/1.90
% 1.67/1.90 -------> usable clausifies to:
% 1.67/1.90
% 1.67/1.90 list(usable).
% 1.67/1.90 0 [] cowlThing(X).
% 1.67/1.90 0 [] -cowlNothing(X).
% 1.67/1.90 0 [] -xsd_string(X)| -xsd_integer(X).
% 1.67/1.90 0 [] xsd_string(X)|xsd_integer(X).
% 1.67/1.90 0 [] -cA(X)|rq(X,$f1(X)).
% 1.67/1.90 0 [] -cA(X)|cowlThing($f1(X)).
% 1.67/1.90 0 [] cA(X)| -rq(X,Y)| -cowlThing(Y).
% 1.67/1.90 0 [] -cAorB(X)|rs(X,$f2(X)).
% 1.67/1.90 0 [] -cAorB(X)|cowlThing($f2(X)).
% 1.67/1.90 0 [] cAorB(X)| -rs(X,Y)| -cowlThing(Y).
% 1.67/1.90 0 [] -cB(X)|rr(X,$f3(X)).
% 1.67/1.90 0 [] -cB(X)|cowlThing($f3(X)).
% 1.67/1.90 0 [] cB(X)| -rr(X,Y)| -cowlThing(Y).
% 1.67/1.90 0 [] -cNothing(X)|rp(X,$f4(X)).
% 1.67/1.90 0 [] -cNothing(X)| -rp(X,Y).
% 1.67/1.90 0 [] -cnotA(X)| -rq(X,Y)|cNothing(Y).
% 1.67/1.90 0 [] cnotA(X)|rq(X,$f5(X)).
% 1.67/1.90 0 [] cnotA(X)| -cNothing($f5(X)).
% 1.67/1.90 0 [] -cnotAorB(X)| -rs(X,Y)|cNothing(Y).
% 1.67/1.90 0 [] cnotAorB(X)|rs(X,$f6(X)).
% 1.67/1.90 0 [] cnotAorB(X)| -cNothing($f6(X)).
% 1.67/1.90 0 [] -cnotAorB(X)|cnotB(X).
% 1.67/1.90 0 [] -cnotAorB(X)|cnotA(X).
% 1.67/1.90 0 [] cnotAorB(X)| -cnotB(X)| -cnotA(X).
% 1.67/1.90 0 [] -cnotB(X)| -rr(X,Y)|cNothing(Y).
% 1.67/1.90 0 [] cnotB(X)|rr(X,$f7(X)).
% 1.67/1.90 0 [] cnotB(X)| -cNothing($f7(X)).
% 1.67/1.90 0 [] -cowlThing($c1)|cowlNothing($c1)|xsd_string($c2)| -xsd_integer($c2)|cAorB($c3)|cB($c3)|cA($c3).
% 1.67/1.90 0 [] -cowlThing($c1)|cowlNothing($c1)|xsd_string($c2)| -xsd_integer($c2)| -cAorB($c3)| -cB($c3).
% 1.67/1.90 0 [] -cowlThing($c1)|cowlNothing($c1)|xsd_string($c2)| -xsd_integer($c2)| -cAorB($c3)| -cA($c3).
% 1.67/1.90 0 [] -cowlThing($c1)|cowlNothing($c1)| -xsd_string($c2)|xsd_integer($c2)|cAorB($c3)|cB($c3)|cA($c3).
% 1.67/1.90 0 [] -cowlThing($c1)|cowlNothing($c1)| -xsd_string($c2)|xsd_integer($c2)| -cAorB($c3)| -cB($c3).
% 1.67/1.90 0 [] -cowlThing($c1)|cowlNothing($c1)| -xsd_string($c2)|xsd_integer($c2)| -cAorB($c3)| -cA($c3).
% 1.67/1.90 end_of_list.
% 1.67/1.90
% 1.67/1.90 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=7.
% 1.67/1.90
% 1.67/1.90 This is a non-Horn set without equality. The strategy will
% 1.67/1.90 be ordered hyper_res, unit deletion, and factoring, with
% 1.67/1.90 satellites in sos and with nuclei in usable.
% 1.67/1.90
% 1.67/1.90 dependent: set(hyper_res).
% 1.67/1.90 dependent: set(factor).
% 1.67/1.90 dependent: set(unit_deletion).
% 1.67/1.90
% 1.67/1.90 ------------> process usable:
% 1.67/1.90 ** KEPT (pick-wt=2): 1 [] -cowlNothing(A).
% 1.67/1.90 ** KEPT (pick-wt=4): 2 [] -xsd_string(A)| -xsd_integer(A).
% 1.67/1.90 ** KEPT (pick-wt=6): 3 [] -cA(A)|rq(A,$f1(A)).
% 1.67/1.90 ** KEPT (pick-wt=5): 4 [] -cA(A)|cowlThing($f1(A)).
% 1.67/1.90 ** KEPT (pick-wt=7): 5 [] cA(A)| -rq(A,B)| -cowlThing(B).
% 1.67/1.90 ** KEPT (pick-wt=6): 6 [] -cAorB(A)|rs(A,$f2(A)).
% 1.67/1.90 ** KEPT (pick-wt=5): 7 [] -cAorB(A)|cowlThing($f2(A)).
% 1.67/1.90 ** KEPT (pick-wt=7): 8 [] cAorB(A)| -rs(A,B)| -cowlThing(B).
% 1.67/1.90 ** KEPT (pick-wt=6): 9 [] -cB(A)|rr(A,$f3(A)).
% 1.67/1.90 ** KEPT (pick-wt=5): 10 [] -cB(A)|cowlThing($f3(A)).
% 1.67/1.90 ** KEPT (pick-wt=7): 11 [] cB(A)| -rr(A,B)| -cowlThing(B).
% 1.67/1.90 ** KEPT (pick-wt=6): 12 [] -cNothing(A)|rp(A,$f4(A)).
% 1.67/1.90 ** KEPT (pick-wt=5): 13 [] -cNothing(A)| -rp(A,B).
% 1.67/1.90 ** KEPT (pick-wt=7): 14 [] -cnotA(A)| -rq(A,B)|cNothing(B).
% 1.67/1.90 ** KEPT (pick-wt=5): 15 [] cnotA(A)| -cNothing($f5(A)).
% 1.67/1.90 ** KEPT (pick-wt=7): 16 [] -cnotAorB(A)| -rs(A,B)|cNothing(B).
% 1.67/1.90 ** KEPT (pick-wt=5): 17 [] cnotAorB(A)| -cNothing($f6(A)).
% 1.67/1.91 ** KEPT (pick-wt=4): 18 [] -cnotAorB(A)|cnotB(A).
% 1.67/1.91 ** KEPT (pick-wt=4): 19 [] -cnotAorB(A)|cnotA(A).
% 1.67/1.91 ** KEPT (pick-wt=6): 20 [] cnotAorB(A)| -cnotB(A)| -cnotA(A).
% 1.67/1.91 ** KEPT (pick-wt=7): 21 [] -cnotB(A)| -rr(A,B)|cNothing(B).
% 1.67/1.91 ** KEPT (pick-wt=5): 22 [] cnotB(A)| -cNothing($f7(A)).
% 1.67/1.91 ** KEPT (pick-wt=12): 24 [copy,23,unit_del,1] -cowlThing($c1)|xsd_string($c2)| -xsd_integer($c2)|cAorB($c3)|cB($c3)|cA($c3).
% 1.67/1.91 ** KEPT (pick-wt=10): 26 [copy,25,unit_del,1] -cowlThing($c1)|xsd_string($c2)| -xsd_integer($c2)| -cAorB($c3)| -cB($c3).
% 1.67/1.91 ** KEPT (pick-wt=10): 28 [copy,27,unit_del,1] -cowlThing($c1)|xsd_string($c2)| -xsd_integer($c2)| -cAorB($c3)| -cA($c3).
% 1.67/1.91 ** KEPT (pick-wt=12): 30 [copy,29,unit_del,1] -cowlThing($c1)| -xsd_string($c2)|xsd_integer($c2)|cAorB($c3)|cB($c3)|cA($c3).
% 1.67/1.91 ** KEPT (pick-wt=10): 32 [copy,31,unit_del,1] -cowlThing($c1)| -xsd_string($c2)|xsd_integer($c2)| -cAorB($c3)| -cB($c3).
% 1.67/1.91 ** KEPT (pick-wt=10): 34 [copy,33,unit_del,1] -cowlThing($c1)| -xsd_string($c2)|xsd_integer($c2)| -cAorB($c3)| -cA($c3).
% 1.67/1.91
% 1.67/1.91 ------------> process sos:
% 1.67/1.91 ** KEPT (pick-wt=2): 35 [] cowlThing(A).
% 1.67/1.91 ** KEPT (pick-wt=4): 36 [] xsd_string(A)|xsd_integer(A).
% 1.67/1.91 ** KEPT (pick-wt=6): 37 [] cnotA(A)|rq(A,$f5(A)).
% 1.67/1.91 ** KEPT (pick-wt=6): 38 [] cnotAorB(A)|rs(A,$f6(A)).
% 1.67/1.91 ** KEPT (pick-wt=6): 39 [] cnotB(A)|rr(A,$f7(A)).
% 1.67/1.91 35 back subsumes 10.
% 1.67/1.91 35 back subsumes 7.
% 1.67/1.91 35 back subsumes 4.
% 1.67/1.91
% 1.67/1.91 ======= end of input processing =======
% 1.67/1.91
% 1.67/1.91 =========== start of search ===========
% 1.67/1.91
% 1.67/1.91 -------- PROOF --------
% 1.67/1.91
% 1.67/1.91 -----> EMPTY CLAUSE at 0.01 sec ----> 212 [hyper,211,2,209] $F.
% 1.67/1.91
% 1.67/1.91 Length of proof is 105. Level of proof is 85.
% 1.67/1.91
% 1.67/1.91 ---------------- PROOF ----------------
% 1.67/1.91 % SZS status Theorem
% 1.67/1.91 % SZS output start Refutation
% See solution above
% 1.67/1.91 ------------ end of proof -------------
% 1.67/1.91
% 1.67/1.91
% 1.67/1.91 Search stopped by max_proofs option.
% 1.67/1.91
% 1.67/1.91
% 1.67/1.91 Search stopped by max_proofs option.
% 1.67/1.91
% 1.67/1.91 ============ end of search ============
% 1.67/1.91
% 1.67/1.91 -------------- statistics -------------
% 1.67/1.91 clauses given 134
% 1.67/1.91 clauses generated 541
% 1.67/1.91 clauses kept 205
% 1.67/1.91 clauses forward subsumed 368
% 1.67/1.91 clauses back subsumed 167
% 1.67/1.91 Kbytes malloced 976
% 1.67/1.91
% 1.67/1.91 ----------- times (seconds) -----------
% 1.67/1.91 user CPU time 0.01 (0 hr, 0 min, 0 sec)
% 1.67/1.91 system CPU time 0.00 (0 hr, 0 min, 0 sec)
% 1.67/1.91 wall-clock time 1 (0 hr, 0 min, 1 sec)
% 1.67/1.91
% 1.67/1.91 That finishes the proof of the theorem.
% 1.67/1.91
% 1.67/1.91 Process 8787 finished Wed Jul 27 03:25:24 2022
% 1.67/1.91 Otter interrupted
% 1.67/1.91 PROOF FOUND
%------------------------------------------------------------------------------