%------------------------------------------------------------------------------
% File : Otter---3.3
% Problem : KRS167+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : otter-tptp-script %s
% Computer : n029.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:29 EDT 2022
% Result : Theorem 3.59s 3.79s
% Output : Refutation 3.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 19
% Syntax : Number of clauses : 95 ( 22 unt; 63 nHn; 92 RR)
% Number of literals : 224 ( 20 equ; 48 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-1 aty)
% Number of variables : 30 ( 13 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(9,axiom,
~ cowlNothing(A),
file('KRS167+1.p',unknown),
[] ).
cnf(10,axiom,
( ~ xsd_string(A)
| ~ xsd_integer(A) ),
file('KRS167+1.p',unknown),
[] ).
cnf(11,axiom,
( ~ cc1(A)
| rp(A,dollar_f1(A)) ),
file('KRS167+1.p',unknown),
[] ).
cnf(12,axiom,
( ~ cc1(A)
| ~ rp(A,B)
| ~ rp(A,C)
| B = C ),
file('KRS167+1.p',unknown),
[] ).
cnf(13,axiom,
( cc1(A)
| ~ rp(A,B)
| rp(A,dollar_f3(A)) ),
file('KRS167+1.p',unknown),
[] ).
cnf(14,axiom,
( cc1(A)
| ~ rp(A,B)
| rp(A,dollar_f2(A)) ),
file('KRS167+1.p',unknown),
[] ).
cnf(15,axiom,
( cc1(A)
| ~ rp(A,B)
| dollar_f3(A) != dollar_f2(A) ),
file('KRS167+1.p',unknown),
[] ).
cnf(16,axiom,
( ~ cc2(A)
| rp(A,dollar_f4(A)) ),
file('KRS167+1.p',unknown),
[] ).
cnf(17,axiom,
( ~ cc2(A)
| ~ rp(A,B)
| ~ rp(A,C)
| B = C ),
file('KRS167+1.p',unknown),
[] ).
cnf(18,axiom,
( cc2(A)
| ~ rp(A,B)
| rp(A,dollar_f6(A)) ),
file('KRS167+1.p',unknown),
[] ).
cnf(19,axiom,
( cc2(A)
| ~ rp(A,B)
| rp(A,dollar_f5(A)) ),
file('KRS167+1.p',unknown),
[] ).
cnf(20,axiom,
( cc2(A)
| ~ rp(A,B)
| dollar_f6(A) != dollar_f5(A) ),
file('KRS167+1.p',unknown),
[] ).
cnf(21,axiom,
( ~ cowlThing(dollar_c1)
| cowlNothing(dollar_c1)
| xsd_string(dollar_c2)
| ~ xsd_integer(dollar_c2)
| cc1(dollar_c3)
| cc2(dollar_c3) ),
file('KRS167+1.p',unknown),
[] ).
cnf(22,plain,
( ~ cowlThing(dollar_c1)
| xsd_string(dollar_c2)
| ~ xsd_integer(dollar_c2)
| cc1(dollar_c3)
| cc2(dollar_c3) ),
inference(unit_del,[status(thm)],[inference(copy,[status(thm)],[21]),9]),
[iquote('copy,21,unit_del,9')] ).
cnf(23,axiom,
( ~ cowlThing(dollar_c1)
| cowlNothing(dollar_c1)
| xsd_string(dollar_c2)
| ~ xsd_integer(dollar_c2)
| ~ cc1(dollar_c3)
| ~ cc2(dollar_c3) ),
file('KRS167+1.p',unknown),
[] ).
cnf(24,plain,
( ~ cowlThing(dollar_c1)
| xsd_string(dollar_c2)
| ~ xsd_integer(dollar_c2)
| ~ cc1(dollar_c3)
| ~ cc2(dollar_c3) ),
inference(unit_del,[status(thm)],[inference(copy,[status(thm)],[23]),9]),
[iquote('copy,23,unit_del,9')] ).
cnf(25,axiom,
( ~ cowlThing(dollar_c1)
| cowlNothing(dollar_c1)
| ~ xsd_string(dollar_c2)
| xsd_integer(dollar_c2)
| cc1(dollar_c3)
| cc2(dollar_c3) ),
file('KRS167+1.p',unknown),
[] ).
cnf(26,plain,
( ~ cowlThing(dollar_c1)
| ~ xsd_string(dollar_c2)
| xsd_integer(dollar_c2)
| cc1(dollar_c3)
| cc2(dollar_c3) ),
inference(unit_del,[status(thm)],[inference(copy,[status(thm)],[25]),9]),
[iquote('copy,25,unit_del,9')] ).
cnf(27,axiom,
( ~ cowlThing(dollar_c1)
| cowlNothing(dollar_c1)
| ~ xsd_string(dollar_c2)
| xsd_integer(dollar_c2)
| ~ cc1(dollar_c3)
| ~ cc2(dollar_c3) ),
file('KRS167+1.p',unknown),
[] ).
cnf(28,plain,
( ~ cowlThing(dollar_c1)
| ~ xsd_string(dollar_c2)
| xsd_integer(dollar_c2)
| ~ cc1(dollar_c3)
| ~ cc2(dollar_c3) ),
inference(unit_del,[status(thm)],[inference(copy,[status(thm)],[27]),9]),
[iquote('copy,27,unit_del,9')] ).
cnf(31,axiom,
A = A,
file('KRS167+1.p',unknown),
[] ).
cnf(32,axiom,
cowlThing(A),
file('KRS167+1.p',unknown),
[] ).
cnf(33,axiom,
( xsd_string(A)
| xsd_integer(A) ),
file('KRS167+1.p',unknown),
[] ).
cnf(34,plain,
( xsd_integer(dollar_c2)
| cc1(dollar_c3)
| cc2(dollar_c3) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[33,26,32])]),
[iquote('hyper,33,26,32,factor_simp')] ).
cnf(35,plain,
( cc1(dollar_c3)
| cc2(dollar_c3)
| xsd_string(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[34,22,32])])]),
[iquote('hyper,34,22,32,factor_simp,factor_simp')] ).
cnf(42,plain,
( cc1(dollar_c3)
| cc2(dollar_c3) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[35,10,34])])]),
[iquote('hyper,35,10,34,factor_simp,factor_simp')] ).
cnf(56,plain,
( cc1(dollar_c3)
| rp(dollar_c3,dollar_f4(dollar_c3)) ),
inference(hyper,[status(thm)],[42,16]),
[iquote('hyper,42,16')] ).
cnf(61,plain,
( rp(dollar_c3,dollar_f4(dollar_c3))
| rp(dollar_c3,dollar_f1(dollar_c3)) ),
inference(hyper,[status(thm)],[56,11]),
[iquote('hyper,56,11')] ).
cnf(72,plain,
( rp(dollar_c3,dollar_f1(dollar_c3))
| cc1(dollar_c3)
| rp(dollar_c3,dollar_f2(dollar_c3)) ),
inference(hyper,[status(thm)],[61,14]),
[iquote('hyper,61,14')] ).
cnf(73,plain,
( rp(dollar_c3,dollar_f1(dollar_c3))
| cc1(dollar_c3)
| rp(dollar_c3,dollar_f3(dollar_c3)) ),
inference(hyper,[status(thm)],[61,13]),
[iquote('hyper,61,13')] ).
cnf(74,plain,
( rp(dollar_c3,dollar_f4(dollar_c3))
| cc2(dollar_c3)
| rp(dollar_c3,dollar_f5(dollar_c3)) ),
inference(hyper,[status(thm)],[61,19]),
[iquote('hyper,61,19')] ).
cnf(75,plain,
( rp(dollar_c3,dollar_f4(dollar_c3))
| cc2(dollar_c3)
| rp(dollar_c3,dollar_f6(dollar_c3)) ),
inference(hyper,[status(thm)],[61,18]),
[iquote('hyper,61,18')] ).
cnf(172,plain,
( rp(dollar_c3,dollar_f1(dollar_c3))
| rp(dollar_c3,dollar_f2(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[72,11])]),
[iquote('hyper,72,11,factor_simp')] ).
cnf(175,plain,
( rp(dollar_c3,dollar_f2(dollar_c3))
| cc1(dollar_c3) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[172,14])]),
[iquote('hyper,172,14,factor_simp')] ).
cnf(231,plain,
( rp(dollar_c3,dollar_f1(dollar_c3))
| rp(dollar_c3,dollar_f3(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[73,11])]),
[iquote('hyper,73,11,factor_simp')] ).
cnf(234,plain,
( rp(dollar_c3,dollar_f3(dollar_c3))
| cc1(dollar_c3) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[231,13])]),
[iquote('hyper,231,13,factor_simp')] ).
cnf(268,plain,
( rp(dollar_c3,dollar_f4(dollar_c3))
| rp(dollar_c3,dollar_f5(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[74,16])]),
[iquote('hyper,74,16,factor_simp')] ).
cnf(285,plain,
( rp(dollar_c3,dollar_f5(dollar_c3))
| cc2(dollar_c3) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[268,19])]),
[iquote('hyper,268,19,factor_simp')] ).
cnf(307,plain,
( rp(dollar_c3,dollar_f5(dollar_c3))
| xsd_integer(dollar_c2)
| rp(dollar_c3,dollar_f3(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[285,28,32,33,234])]),
[iquote('hyper,285,28,32,33,234,factor_simp')] ).
cnf(308,plain,
( rp(dollar_c3,dollar_f5(dollar_c3))
| xsd_integer(dollar_c2)
| rp(dollar_c3,dollar_f2(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[285,28,32,33,175])]),
[iquote('hyper,285,28,32,33,175,factor_simp')] ).
cnf(333,plain,
( rp(dollar_c3,dollar_f4(dollar_c3))
| rp(dollar_c3,dollar_f6(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[75,16])]),
[iquote('hyper,75,16,factor_simp')] ).
cnf(352,plain,
( rp(dollar_c3,dollar_f6(dollar_c3))
| cc2(dollar_c3) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[333,18])]),
[iquote('hyper,333,18,factor_simp')] ).
cnf(359,plain,
( rp(dollar_c3,dollar_f4(dollar_c3))
| dollar_f6(dollar_c3) = dollar_f5(dollar_c3) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[333,12,56,268])])]),
[iquote('hyper,333,12,56,268,factor_simp,factor_simp')] ).
cnf(377,plain,
( rp(dollar_c3,dollar_f6(dollar_c3))
| xsd_integer(dollar_c2)
| rp(dollar_c3,dollar_f3(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[352,28,32,33,234])]),
[iquote('hyper,352,28,32,33,234,factor_simp')] ).
cnf(378,plain,
( rp(dollar_c3,dollar_f6(dollar_c3))
| xsd_integer(dollar_c2)
| rp(dollar_c3,dollar_f2(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[352,28,32,33,175])]),
[iquote('hyper,352,28,32,33,175,factor_simp')] ).
cnf(399,plain,
( cc2(dollar_c3)
| ~ rp(dollar_c3,A)
| rp(dollar_c3,dollar_f4(dollar_c3)) ),
inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[359,20]),31]),
[iquote('para_from,359.2.1,20.3.1,unit_del,31')] ).
cnf(417,plain,
( cc2(dollar_c3)
| rp(dollar_c3,dollar_f4(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[399,333])]),
[iquote('hyper,399,333,factor_simp')] ).
cnf(421,plain,
rp(dollar_c3,dollar_f4(dollar_c3)),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[417,16])]),
[iquote('hyper,417,16,factor_simp')] ).
cnf(460,plain,
( rp(dollar_c3,dollar_f5(dollar_c3))
| rp(dollar_c3,dollar_f3(dollar_c3))
| xsd_string(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[307,24,32,234,285])])]),
[iquote('hyper,307,24,32,234,285,factor_simp,factor_simp')] ).
cnf(480,plain,
( rp(dollar_c3,dollar_f5(dollar_c3))
| rp(dollar_c3,dollar_f2(dollar_c3))
| xsd_string(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[308,24,32,175,285])])]),
[iquote('hyper,308,24,32,175,285,factor_simp,factor_simp')] ).
cnf(499,plain,
( rp(dollar_c3,dollar_f6(dollar_c3))
| rp(dollar_c3,dollar_f3(dollar_c3))
| xsd_string(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[377,24,32,234,352])])]),
[iquote('hyper,377,24,32,234,352,factor_simp,factor_simp')] ).
cnf(524,plain,
( rp(dollar_c3,dollar_f6(dollar_c3))
| rp(dollar_c3,dollar_f2(dollar_c3))
| xsd_string(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[378,24,32,175,352])])]),
[iquote('hyper,378,24,32,175,352,factor_simp,factor_simp')] ).
cnf(546,plain,
( rp(dollar_c3,dollar_f5(dollar_c3))
| rp(dollar_c3,dollar_f3(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[460,10,307])])]),
[iquote('hyper,460,10,307,factor_simp,factor_simp')] ).
cnf(618,plain,
( rp(dollar_c3,dollar_f5(dollar_c3))
| rp(dollar_c3,dollar_f2(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[480,10,308])])]),
[iquote('hyper,480,10,308,factor_simp,factor_simp')] ).
cnf(633,plain,
( rp(dollar_c3,dollar_f5(dollar_c3))
| dollar_f3(dollar_c3) = dollar_f2(dollar_c3) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[618,17,285,546])])]),
[iquote('hyper,618,17,285,546,factor_simp,factor_simp')] ).
cnf(693,plain,
( cc1(dollar_c3)
| ~ rp(dollar_c3,A)
| rp(dollar_c3,dollar_f5(dollar_c3)) ),
inference(unit_del,[status(thm)],[inference(para_from,[status(thm),theory(equality)],[633,15]),31]),
[iquote('para_from,633.2.1,15.3.1,unit_del,31')] ).
cnf(708,plain,
( cc1(dollar_c3)
| rp(dollar_c3,dollar_f5(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[693,618])]),
[iquote('hyper,693,618,factor_simp')] ).
cnf(710,plain,
( rp(dollar_c3,dollar_f5(dollar_c3))
| xsd_integer(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[708,28,32,33,285])])]),
[iquote('hyper,708,28,32,33,285,factor_simp,factor_simp')] ).
cnf(721,plain,
( rp(dollar_c3,dollar_f5(dollar_c3))
| xsd_string(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[710,24,32,708,285])])]),
[iquote('hyper,710,24,32,708,285,factor_simp,factor_simp')] ).
cnf(730,plain,
rp(dollar_c3,dollar_f5(dollar_c3)),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[721,10,710])]),
[iquote('hyper,721,10,710,factor_simp')] ).
cnf(806,plain,
( dollar_f5(dollar_c3) = dollar_f4(dollar_c3)
| cc1(dollar_c3) ),
inference(flip,[status(thm),theory(equality)],[inference(hyper,[status(thm)],[730,17,42,421])]),
[iquote('hyper,730,17,42,421,flip.1')] ).
cnf(820,plain,
dollar_f5(dollar_c3) = dollar_f4(dollar_c3),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[806,12,730,421])]),
[iquote('hyper,806,12,730,421,factor_simp')] ).
cnf(824,plain,
( rp(dollar_c3,dollar_f6(dollar_c3))
| rp(dollar_c3,dollar_f3(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[499,10,377])])]),
[iquote('hyper,499,10,377,factor_simp,factor_simp')] ).
cnf(859,plain,
( rp(dollar_c3,dollar_f3(dollar_c3))
| dollar_f6(dollar_c3) = dollar_f4(dollar_c3) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[824,12,234,421])]),
[iquote('hyper,824,12,234,421,factor_simp')] ).
cnf(892,plain,
( cc2(dollar_c3)
| ~ rp(dollar_c3,A)
| rp(dollar_c3,dollar_f3(dollar_c3)) ),
inference(unit_del,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[859,20]),820]),31]),
[iquote('para_from,859.2.1,20.3.1,demod,820,unit_del,31')] ).
cnf(975,plain,
( cc2(dollar_c3)
| rp(dollar_c3,dollar_f3(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[892,824])]),
[iquote('hyper,892,824,factor_simp')] ).
cnf(976,plain,
( rp(dollar_c3,dollar_f3(dollar_c3))
| xsd_integer(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[975,28,32,33,234])])]),
[iquote('hyper,975,28,32,33,234,factor_simp,factor_simp')] ).
cnf(985,plain,
( rp(dollar_c3,dollar_f3(dollar_c3))
| xsd_string(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[976,24,32,234,975])])]),
[iquote('hyper,976,24,32,234,975,factor_simp,factor_simp')] ).
cnf(994,plain,
rp(dollar_c3,dollar_f3(dollar_c3)),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[985,10,976])]),
[iquote('hyper,985,10,976,factor_simp')] ).
cnf(1021,plain,
( dollar_f4(dollar_c3) = dollar_f3(dollar_c3)
| cc1(dollar_c3) ),
inference(hyper,[status(thm)],[994,17,42,421]),
[iquote('hyper,994,17,42,421')] ).
cnf(1034,plain,
dollar_f4(dollar_c3) = dollar_f3(dollar_c3),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[1021,12,994,421])]),
[iquote('hyper,1021,12,994,421,factor_simp')] ).
cnf(1038,plain,
dollar_f5(dollar_c3) = dollar_f3(dollar_c3),
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[820]),1034]),
[iquote('back_demod,819,demod,1034')] ).
cnf(1058,plain,
( rp(dollar_c3,dollar_f6(dollar_c3))
| rp(dollar_c3,dollar_f2(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[524,10,378])])]),
[iquote('hyper,524,10,378,factor_simp,factor_simp')] ).
cnf(1059,plain,
( rp(dollar_c3,dollar_f2(dollar_c3))
| dollar_f6(dollar_c3) = dollar_f3(dollar_c3) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[1058,12,175,994])]),
[iquote('hyper,1058,12,175,994,factor_simp')] ).
cnf(1089,plain,
( cc2(dollar_c3)
| ~ rp(dollar_c3,A)
| rp(dollar_c3,dollar_f2(dollar_c3)) ),
inference(unit_del,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[1059,20]),1038]),31]),
[iquote('para_from,1059.2.1,20.3.1,demod,1038,unit_del,31')] ).
cnf(1113,plain,
( cc2(dollar_c3)
| rp(dollar_c3,dollar_f2(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[1089,1058])]),
[iquote('hyper,1089,1058,factor_simp')] ).
cnf(1114,plain,
( rp(dollar_c3,dollar_f2(dollar_c3))
| xsd_integer(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[1113,28,32,33,175])])]),
[iquote('hyper,1113,28,32,33,175,factor_simp,factor_simp')] ).
cnf(1128,plain,
( rp(dollar_c3,dollar_f2(dollar_c3))
| xsd_string(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[1114,24,32,175,1113])])]),
[iquote('hyper,1114,24,32,175,1113,factor_simp,factor_simp')] ).
cnf(1137,plain,
rp(dollar_c3,dollar_f2(dollar_c3)),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[1128,10,1114])]),
[iquote('hyper,1128,10,1114,factor_simp')] ).
cnf(1139,plain,
( dollar_f3(dollar_c3) = dollar_f2(dollar_c3)
| cc1(dollar_c3) ),
inference(hyper,[status(thm)],[1137,17,42,994]),
[iquote('hyper,1137,17,42,994')] ).
cnf(1148,plain,
dollar_f3(dollar_c3) = dollar_f2(dollar_c3),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[1139,12,1137,994])]),
[iquote('hyper,1139,12,1137,994,factor_simp')] ).
cnf(1151,plain,
dollar_f5(dollar_c3) = dollar_f2(dollar_c3),
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[1038]),1148]),
[iquote('back_demod,1037,demod,1148')] ).
cnf(1157,plain,
cc1(dollar_c3),
inference(hyper,[status(thm)],[1148,15,1137]),
[iquote('hyper,1147,15,1137')] ).
cnf(1160,plain,
( xsd_integer(dollar_c2)
| rp(dollar_c3,dollar_f6(dollar_c3)) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[1157,28,32,33,352])]),
[iquote('hyper,1157,28,32,33,352,factor_simp')] ).
cnf(1161,plain,
rp(dollar_c3,dollar_f1(dollar_c3)),
inference(hyper,[status(thm)],[1157,11]),
[iquote('hyper,1157,11')] ).
cnf(1166,plain,
dollar_f2(dollar_c3) = dollar_f1(dollar_c3),
inference(hyper,[status(thm)],[1161,12,1157,1137]),
[iquote('hyper,1161,12,1157,1137')] ).
cnf(1174,plain,
dollar_f5(dollar_c3) = dollar_f1(dollar_c3),
inference(demod,[status(thm),theory(equality)],[inference(back_demod,[status(thm)],[1151]),1166]),
[iquote('back_demod,1151,demod,1166')] ).
cnf(1213,plain,
( rp(dollar_c3,dollar_f6(dollar_c3))
| xsd_string(dollar_c2) ),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[1160,24,32,1157,352])]),
[iquote('hyper,1160,24,32,1157,352,factor_simp')] ).
cnf(1286,plain,
rp(dollar_c3,dollar_f6(dollar_c3)),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[1213,10,1160])]),
[iquote('hyper,1213,10,1160,factor_simp')] ).
cnf(1287,plain,
dollar_f6(dollar_c3) = dollar_f1(dollar_c3),
inference(flip,[status(thm),theory(equality)],[inference(hyper,[status(thm)],[1286,12,1157,1161])]),
[iquote('hyper,1286,12,1157,1161,flip.1')] ).
cnf(1291,plain,
( cc2(dollar_c3)
| ~ rp(dollar_c3,A) ),
inference(unit_del,[status(thm)],[inference(demod,[status(thm),theory(equality)],[inference(para_from,[status(thm),theory(equality)],[1287,20]),1174]),31]),
[iquote('para_from,1287.1.1,20.3.1,demod,1174,unit_del,31')] ).
cnf(1292,plain,
cc2(dollar_c3),
inference(hyper,[status(thm)],[1291,1161]),
[iquote('hyper,1291,1161')] ).
cnf(1301,plain,
xsd_integer(dollar_c2),
inference(factor_simp,[status(thm)],[inference(hyper,[status(thm)],[1292,28,32,33,1157])]),
[iquote('hyper,1292,28,32,33,1157,factor_simp')] ).
cnf(1304,plain,
xsd_string(dollar_c2),
inference(hyper,[status(thm)],[1301,24,32,1157,1292]),
[iquote('hyper,1301,24,32,1157,1292')] ).
cnf(1307,plain,
$false,
inference(hyper,[status(thm)],[1304,10,1301]),
[iquote('hyper,1304,10,1301')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : KRS167+1 : TPTP v8.1.0. Released v3.1.0.
% 0.06/0.12 % Command : otter-tptp-script %s
% 0.12/0.33 % Computer : n029.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:34:14 EDT 2022
% 0.12/0.33 % CPUTime :
% 1.75/1.97 ----- Otter 3.3f, August 2004 -----
% 1.75/1.97 The process was started by sandbox on n029.cluster.edu,
% 1.75/1.97 Wed Jul 27 03:34:14 2022
% 1.75/1.97 The command was "./otter". The process ID is 31567.
% 1.75/1.97
% 1.75/1.97 set(prolog_style_variables).
% 1.75/1.97 set(auto).
% 1.75/1.97 dependent: set(auto1).
% 1.75/1.97 dependent: set(process_input).
% 1.75/1.97 dependent: clear(print_kept).
% 1.75/1.97 dependent: clear(print_new_demod).
% 1.75/1.97 dependent: clear(print_back_demod).
% 1.75/1.97 dependent: clear(print_back_sub).
% 1.75/1.97 dependent: set(control_memory).
% 1.75/1.97 dependent: assign(max_mem, 12000).
% 1.75/1.97 dependent: assign(pick_given_ratio, 4).
% 1.75/1.97 dependent: assign(stats_level, 1).
% 1.75/1.97 dependent: assign(max_seconds, 10800).
% 1.75/1.97 clear(print_given).
% 1.75/1.97
% 1.75/1.97 formula_list(usable).
% 1.75/1.97 all A (A=A).
% 1.75/1.97 all A B (A=B&cc1(A)->cc1(B)).
% 1.75/1.97 all A B (A=B&cc2(A)->cc2(B)).
% 1.75/1.97 all A B (A=B&cowlNothing(A)->cowlNothing(B)).
% 1.75/1.97 all A B (A=B&cowlThing(A)->cowlThing(B)).
% 1.75/1.97 all A B C (A=B&rp(A,C)->rp(B,C)).
% 1.75/1.97 all A B C (A=B&rp(C,A)->rp(C,B)).
% 1.75/1.97 all A B (A=B&xsd_integer(A)->xsd_integer(B)).
% 1.75/1.97 all A B (A=B&xsd_string(A)->xsd_string(B)).
% 1.75/1.97 all X (cowlThing(X)& -cowlNothing(X)).
% 1.75/1.97 all X (xsd_string(X)<-> -xsd_integer(X)).
% 1.75/1.97 all X (cc1(X)<-> (exists Y0 rp(X,Y0))& (all Y0 Y1 (rp(X,Y0)&rp(X,Y1)->Y0=Y1))).
% 1.75/1.97 all X (cc2(X)<-> (exists Y0 rp(X,Y0))& (all Y0 Y1 (rp(X,Y0)&rp(X,Y1)->Y0=Y1))).
% 1.75/1.97 -((all X (cowlThing(X)& -cowlNothing(X)))& (all X (xsd_string(X)<-> -xsd_integer(X)))& (all X (cc1(X)<->cc2(X)))).
% 1.75/1.97 end_of_list.
% 1.75/1.97
% 1.75/1.97 -------> usable clausifies to:
% 1.75/1.97
% 1.75/1.97 list(usable).
% 1.75/1.97 0 [] A=A.
% 1.75/1.97 0 [] A!=B| -cc1(A)|cc1(B).
% 1.75/1.97 0 [] A!=B| -cc2(A)|cc2(B).
% 1.75/1.97 0 [] A!=B| -cowlNothing(A)|cowlNothing(B).
% 1.75/1.97 0 [] A!=B| -cowlThing(A)|cowlThing(B).
% 1.75/1.97 0 [] A!=B| -rp(A,C)|rp(B,C).
% 1.75/1.97 0 [] A!=B| -rp(C,A)|rp(C,B).
% 1.75/1.97 0 [] A!=B| -xsd_integer(A)|xsd_integer(B).
% 1.75/1.97 0 [] A!=B| -xsd_string(A)|xsd_string(B).
% 1.75/1.97 0 [] cowlThing(X).
% 1.75/1.97 0 [] -cowlNothing(X).
% 1.75/1.97 0 [] -xsd_string(X)| -xsd_integer(X).
% 1.75/1.97 0 [] xsd_string(X)|xsd_integer(X).
% 1.75/1.97 0 [] -cc1(X)|rp(X,$f1(X)).
% 1.75/1.97 0 [] -cc1(X)| -rp(X,Y0)| -rp(X,Y1)|Y0=Y1.
% 1.75/1.97 0 [] cc1(X)| -rp(X,X1)|rp(X,$f3(X)).
% 1.75/1.97 0 [] cc1(X)| -rp(X,X1)|rp(X,$f2(X)).
% 1.75/1.97 0 [] cc1(X)| -rp(X,X1)|$f3(X)!=$f2(X).
% 1.75/1.97 0 [] -cc2(X)|rp(X,$f4(X)).
% 1.75/1.97 0 [] -cc2(X)| -rp(X,Y0)| -rp(X,Y1)|Y0=Y1.
% 1.75/1.97 0 [] cc2(X)| -rp(X,X2)|rp(X,$f6(X)).
% 1.75/1.97 0 [] cc2(X)| -rp(X,X2)|rp(X,$f5(X)).
% 1.75/1.97 0 [] cc2(X)| -rp(X,X2)|$f6(X)!=$f5(X).
% 1.75/1.97 0 [] -cowlThing($c1)|cowlNothing($c1)|xsd_string($c2)| -xsd_integer($c2)|cc1($c3)|cc2($c3).
% 1.75/1.97 0 [] -cowlThing($c1)|cowlNothing($c1)|xsd_string($c2)| -xsd_integer($c2)| -cc1($c3)| -cc2($c3).
% 1.75/1.97 0 [] -cowlThing($c1)|cowlNothing($c1)| -xsd_string($c2)|xsd_integer($c2)|cc1($c3)|cc2($c3).
% 1.75/1.97 0 [] -cowlThing($c1)|cowlNothing($c1)| -xsd_string($c2)|xsd_integer($c2)| -cc1($c3)| -cc2($c3).
% 1.75/1.97 end_of_list.
% 1.75/1.97
% 1.75/1.97 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=6.
% 1.75/1.97
% 1.75/1.97 This ia a non-Horn set with equality. The strategy will be
% 1.75/1.97 Knuth-Bendix, ordered hyper_res, factoring, and unit
% 1.75/1.97 deletion, with positive clauses in sos and nonpositive
% 1.75/1.97 clauses in usable.
% 1.75/1.97
% 1.75/1.97 dependent: set(knuth_bendix).
% 1.75/1.97 dependent: set(anl_eq).
% 1.75/1.97 dependent: set(para_from).
% 1.75/1.97 dependent: set(para_into).
% 1.75/1.97 dependent: clear(para_from_right).
% 1.75/1.97 dependent: clear(para_into_right).
% 1.75/1.97 dependent: set(para_from_vars).
% 1.75/1.97 dependent: set(eq_units_both_ways).
% 1.75/1.97 dependent: set(dynamic_demod_all).
% 1.75/1.97 dependent: set(dynamic_demod).
% 1.75/1.97 dependent: set(order_eq).
% 1.75/1.97 dependent: set(back_demod).
% 1.75/1.97 dependent: set(lrpo).
% 1.75/1.97 dependent: set(hyper_res).
% 1.75/1.97 dependent: set(unit_deletion).
% 1.75/1.97 dependent: set(factor).
% 1.75/1.97
% 1.75/1.97 ------------> process usable:
% 1.75/1.97 ** KEPT (pick-wt=7): 1 [] A!=B| -cc1(A)|cc1(B).
% 1.75/1.97 ** KEPT (pick-wt=7): 2 [] A!=B| -cc2(A)|cc2(B).
% 1.75/1.97 ** KEPT (pick-wt=7): 3 [] A!=B| -cowlNothing(A)|cowlNothing(B).
% 1.75/1.97 ** KEPT (pick-wt=7): 4 [] A!=B| -cowlThing(A)|cowlThing(B).
% 1.75/1.97 ** KEPT (pick-wt=9): 5 [] A!=B| -rp(A,C)|rp(B,C).
% 1.75/1.97 ** KEPT (pick-wt=9): 6 [] A!=B| -rp(C,A)|rp(C,B).
% 1.75/1.97 ** KEPT (pick-wt=7): 7 [] A!=B| -xsd_integer(A)|xsd_integer(B).
% 1.75/1.97 ** KEPT (pick-wt=7): 8 [] A!=B| -xsd_string(A)|xsd_string(B).
% 1.75/1.97 ** KEPT (pick-wt=2): 9 [] -cowlNothing(A).
% 1.75/1.97 ** KEPT (pick-wt=4): 10 [] -xsd_string(A)| -xsd_integer(A).
% 1.75/1.97 ** KEPT (pick-wt=6): 11 [] -cc1(A)|rp(A,$f1(A)).
% 1.75/1.97 ** KEPT (pick-wt=11): 12 [] -cc1(A)| -rp(A,B)| -rp(A,C)|B=C.
% 1.75/1.97 ** KEPT (pick-wt=9): 13 [] cc1(A)| -rp(A,B)|rp(A,$f3(A)).
% 1.75/1.97 ** KEPT (pick-wt=9): 14 [] cc1(A)| -rp(A,B)|rp(A,$f2(A)).
% 3.59/3.79 ** KEPT (pick-wt=10): 15 [] cc1(A)| -rp(A,B)|$f3(A)!=$f2(A).
% 3.59/3.79 ** KEPT (pick-wt=6): 16 [] -cc2(A)|rp(A,$f4(A)).
% 3.59/3.79 ** KEPT (pick-wt=11): 17 [] -cc2(A)| -rp(A,B)| -rp(A,C)|B=C.
% 3.59/3.79 ** KEPT (pick-wt=9): 18 [] cc2(A)| -rp(A,B)|rp(A,$f6(A)).
% 3.59/3.79 ** KEPT (pick-wt=9): 19 [] cc2(A)| -rp(A,B)|rp(A,$f5(A)).
% 3.59/3.79 ** KEPT (pick-wt=10): 20 [] cc2(A)| -rp(A,B)|$f6(A)!=$f5(A).
% 3.59/3.79 ** KEPT (pick-wt=10): 22 [copy,21,unit_del,9] -cowlThing($c1)|xsd_string($c2)| -xsd_integer($c2)|cc1($c3)|cc2($c3).
% 3.59/3.79 ** KEPT (pick-wt=10): 24 [copy,23,unit_del,9] -cowlThing($c1)|xsd_string($c2)| -xsd_integer($c2)| -cc1($c3)| -cc2($c3).
% 3.59/3.79 ** KEPT (pick-wt=10): 26 [copy,25,unit_del,9] -cowlThing($c1)| -xsd_string($c2)|xsd_integer($c2)|cc1($c3)|cc2($c3).
% 3.59/3.79 ** KEPT (pick-wt=10): 28 [copy,27,unit_del,9] -cowlThing($c1)| -xsd_string($c2)|xsd_integer($c2)| -cc1($c3)| -cc2($c3).
% 3.59/3.79 9 back subsumes 3.
% 3.59/3.79
% 3.59/3.79 ------------> process sos:
% 3.59/3.79 ** KEPT (pick-wt=3): 31 [] A=A.
% 3.59/3.79 ** KEPT (pick-wt=2): 32 [] cowlThing(A).
% 3.59/3.79 ** KEPT (pick-wt=4): 33 [] xsd_string(A)|xsd_integer(A).
% 3.59/3.79 Following clause subsumed by 31 during input processing: 0 [copy,31,flip.1] A=A.
% 3.59/3.79 31 back subsumes 30.
% 3.59/3.79 31 back subsumes 29.
% 3.59/3.79 32 back subsumes 4.
% 3.59/3.79
% 3.59/3.79 ======= end of input processing =======
% 3.59/3.79
% 3.59/3.79 =========== start of search ===========
% 3.59/3.79
% 3.59/3.79 -------- PROOF --------
% 3.59/3.79
% 3.59/3.79 -----> EMPTY CLAUSE at 1.82 sec ----> 1307 [hyper,1304,10,1301] $F.
% 3.59/3.79
% 3.59/3.79 Length of proof is 75. Level of proof is 44.
% 3.59/3.79
% 3.59/3.79 ---------------- PROOF ----------------
% 3.59/3.79 % SZS status Theorem
% 3.59/3.79 % SZS output start Refutation
% See solution above
% 3.59/3.79 ------------ end of proof -------------
% 3.59/3.79
% 3.59/3.79
% 3.59/3.79 Search stopped by max_proofs option.
% 3.59/3.79
% 3.59/3.79
% 3.59/3.79 Search stopped by max_proofs option.
% 3.59/3.79
% 3.59/3.79 ============ end of search ============
% 3.59/3.79
% 3.59/3.79 -------------- statistics -------------
% 3.59/3.79 clauses given 114
% 3.59/3.79 clauses generated 13187
% 3.59/3.79 clauses kept 1291
% 3.59/3.79 clauses forward subsumed 12068
% 3.59/3.79 clauses back subsumed 1085
% 3.59/3.79 Kbytes malloced 1953
% 3.59/3.79
% 3.59/3.79 ----------- times (seconds) -----------
% 3.59/3.79 user CPU time 1.82 (0 hr, 0 min, 1 sec)
% 3.59/3.79 system CPU time 0.00 (0 hr, 0 min, 0 sec)
% 3.59/3.79 wall-clock time 3 (0 hr, 0 min, 3 sec)
% 3.59/3.79
% 3.59/3.79 That finishes the proof of the theorem.
% 3.59/3.79
% 3.59/3.79 Process 31567 finished Wed Jul 27 03:34:17 2022
% 3.59/3.79 Otter interrupted
% 3.59/3.79 PROOF FOUND
%------------------------------------------------------------------------------