%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : KRS149+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n024.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 : 600s
% DateTime : Sun Jul 17 03:30:43 EDT 2022
% Result : Theorem 0.75s 0.97s
% Output : Refutation 0.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 30
% Syntax : Number of clauses : 77 ( 30 unt; 14 nHn; 77 RR)
% Number of literals : 198 ( 0 equ; 127 neg)
% Maximal clause size : 12 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 28 ( 27 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-1 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
cowlThing(u),
file('KRS149+1.p',unknown),
[] ).
cnf(2,axiom,
cTEST(iV3102),
file('KRS149+1.p',unknown),
[] ).
cnf(4,axiom,
cTOP(iV3102),
file('KRS149+1.p',unknown),
[] ).
cnf(5,axiom,
~ cowlNothing(u),
file('KRS149+1.p',unknown),
[] ).
cnf(6,axiom,
~ cC42(iV3102),
file('KRS149+1.p',unknown),
[] ).
cnf(7,axiom,
~ cC12(iV3102),
file('KRS149+1.p',unknown),
[] ).
cnf(8,axiom,
~ cC26(iV3102),
file('KRS149+1.p',unknown),
[] ).
cnf(11,axiom,
~ cC16(iV3102),
file('KRS149+1.p',unknown),
[] ).
cnf(12,axiom,
~ cC2(iV3102),
file('KRS149+1.p',unknown),
[] ).
cnf(13,axiom,
~ cC32(iV3102),
file('KRS149+1.p',unknown),
[] ).
cnf(14,axiom,
~ cC100(iV3102),
file('KRS149+1.p',unknown),
[] ).
cnf(15,axiom,
( xsd_string(u)
| xsd_integer(u) ),
file('KRS149+1.p',unknown),
[] ).
cnf(58,axiom,
( ~ cC214(u)
| cC100(u) ),
file('KRS149+1.p',unknown),
[] ).
cnf(59,axiom,
( ~ cC216(u)
| cC64(u) ),
file('KRS149+1.p',unknown),
[] ).
cnf(64,axiom,
( ~ cC46(u)
| cC30(u) ),
file('KRS149+1.p',unknown),
[] ).
cnf(79,axiom,
( ~ cTEST(u)
| cC216(u) ),
file('KRS149+1.p',unknown),
[] ).
cnf(80,axiom,
( ~ cTEST(u)
| cC46(u) ),
file('KRS149+1.p',unknown),
[] ).
cnf(81,axiom,
( ~ xsd_integer(u)
| ~ xsd_string(u) ),
file('KRS149+1.p',unknown),
[] ).
cnf(84,axiom,
( cC10(u)
| cC2(u)
| cC8(u) ),
file('KRS149+1.p',unknown),
[] ).
cnf(107,axiom,
( cC14(u)
| cC2(u)
| cC12(u) ),
file('KRS149+1.p',unknown),
[] ).
cnf(160,axiom,
( cC28(u)
| cC16(u)
| cC26(u) ),
file('KRS149+1.p',unknown),
[] ).
cnf(168,axiom,
( cC44(u)
| cC42(u)
| cC32(u) ),
file('KRS149+1.p',unknown),
[] ).
cnf(175,axiom,
( ~ cC62(u)
| cC60(skf97(v)) ),
file('KRS149+1.p',unknown),
[] ).
cnf(182,axiom,
( ~ cC8(u)
| cC6(skf102(v)) ),
file('KRS149+1.p',unknown),
[] ).
cnf(237,axiom,
( ~ cC64(u)
| cC216(u)
| cC214(u) ),
file('KRS149+1.p',unknown),
[] ).
cnf(249,axiom,
( ~ cC62(u)
| rR1(u,skf97(u)) ),
file('KRS149+1.p',unknown),
[] ).
cnf(250,axiom,
( ~ cTOP(u)
| cC64(u)
| cC62(u) ),
file('KRS149+1.p',unknown),
[] ).
cnf(262,axiom,
( ~ cC60(u)
| ~ rR1(iV3102,u) ),
file('KRS149+1.p',unknown),
[] ).
cnf(340,axiom,
( ~ xsd_string(skc5)
| ~ cowlThing(skc3)
| ~ cC216(iV3102)
| ~ cC46(iV3102)
| ~ cC30(iV3102)
| ~ cC44(iV3102)
| ~ cC28(iV3102)
| ~ cC64(iV3102)
| ~ cC14(iV3102)
| ~ cowlThing(iV3102)
| xsd_integer(skc5)
| cowlNothing(skc4) ),
file('KRS149+1.p',unknown),
[] ).
cnf(341,axiom,
( ~ xsd_integer(skc5)
| ~ cowlThing(skc3)
| ~ cC216(iV3102)
| ~ cC46(iV3102)
| ~ cC30(iV3102)
| ~ cC44(iV3102)
| ~ cC28(iV3102)
| ~ cC64(iV3102)
| ~ cC14(iV3102)
| ~ cowlThing(iV3102)
| xsd_string(skc5)
| cowlNothing(skc4) ),
file('KRS149+1.p',unknown),
[] ).
cnf(342,plain,
( ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| xsd_integer(skc5) ),
inference(mrr,[status(thm)],[340,15,1,5]),
[iquote('0:MRR:340.0,340.1,340.9,340.11,15.1,1.0,1.0,5.0')] ).
cnf(343,plain,
( ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| xsd_string(skc5) ),
inference(mrr,[status(thm)],[341,342,1,5]),
[iquote('0:MRR:341.0,341.1,341.9,341.11,342.7,1.0,1.0,5.0')] ).
cnf(616,plain,
~ cC214(iV3102),
inference(res,[status(thm),theory(equality)],[58,14]),
[iquote('0:Res:58.1,14.0')] ).
cnf(868,plain,
( cC10(iV3102)
| cC8(iV3102) ),
inference(res,[status(thm),theory(equality)],[84,12]),
[iquote('0:Res:84.1,12.0')] ).
cnf(870,plain,
( cC6(skf102(u))
| cC10(iV3102) ),
inference(ems,[status(thm)],[182,868]),
[iquote('0:EmS:182.0,868.1')] ).
cnf(885,plain,
cC10(iV3102),
inference(spt,[spt(split,[position(s1)])],[870]),
[iquote('1:Spt:870.1')] ).
cnf(925,plain,
( cC14(iV3102)
| cC2(iV3102) ),
inference(res,[status(thm),theory(equality)],[107,7]),
[iquote('0:Res:107.2,7.0')] ).
cnf(926,plain,
cC14(iV3102),
inference(mrr,[status(thm)],[925,12]),
[iquote('0:MRR:925.1,12.0')] ).
cnf(927,plain,
( ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| xsd_string(skc5) ),
inference(mrr,[status(thm)],[343,926]),
[iquote('0:MRR:343.0,926.0')] ).
cnf(928,plain,
( ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| xsd_integer(skc5) ),
inference(mrr,[status(thm)],[342,926]),
[iquote('0:MRR:342.0,926.0')] ).
cnf(931,plain,
( cC28(iV3102)
| cC16(iV3102) ),
inference(res,[status(thm),theory(equality)],[160,8]),
[iquote('0:Res:160.2,8.0')] ).
cnf(932,plain,
cC28(iV3102),
inference(mrr,[status(thm)],[931,11]),
[iquote('0:MRR:931.1,11.0')] ).
cnf(933,plain,
( ~ cC64(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| xsd_string(skc5) ),
inference(mrr,[status(thm)],[927,932]),
[iquote('0:MRR:927.1,932.0')] ).
cnf(934,plain,
( ~ cC64(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| xsd_integer(skc5) ),
inference(mrr,[status(thm)],[928,932]),
[iquote('0:MRR:928.1,932.0')] ).
cnf(955,plain,
( cC44(iV3102)
| cC32(iV3102) ),
inference(res,[status(thm),theory(equality)],[168,6]),
[iquote('0:Res:168.1,6.0')] ).
cnf(956,plain,
cC44(iV3102),
inference(mrr,[status(thm)],[955,13]),
[iquote('0:MRR:955.1,13.0')] ).
cnf(957,plain,
( ~ cC64(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| xsd_string(skc5) ),
inference(mrr,[status(thm)],[933,956]),
[iquote('0:MRR:933.1,956.0')] ).
cnf(958,plain,
( ~ cC64(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| xsd_integer(skc5) ),
inference(mrr,[status(thm)],[934,956]),
[iquote('0:MRR:934.1,956.0')] ).
cnf(1423,plain,
( ~ cC62(iV3102)
| ~ cC60(skf97(iV3102)) ),
inference(res,[status(thm),theory(equality)],[249,262]),
[iquote('0:Res:249.1,262.1')] ).
cnf(1428,plain,
~ cC62(iV3102),
inference(mrr,[status(thm)],[1423,175]),
[iquote('0:MRR:1423.1,175.1')] ).
cnf(1552,plain,
( ~ cTOP(iV3102)
| cC64(iV3102) ),
inference(sor,[status(thm)],[1428,250]),
[iquote('0:SoR:1428.0,250.2')] ).
cnf(1554,plain,
cC64(iV3102),
inference(ssi,[status(thm)],[1552,4,2,885,926,932,956]),
[iquote('1:SSi:1552.0,4.0,2.0,885.0,926.0,932.0,956.0')] ).
cnf(1555,plain,
( ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| xsd_string(skc5) ),
inference(mrr,[status(thm)],[957,1554]),
[iquote('1:MRR:957.0,1554.0')] ).
cnf(1556,plain,
( ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| xsd_integer(skc5) ),
inference(mrr,[status(thm)],[958,1554]),
[iquote('1:MRR:958.0,1554.0')] ).
cnf(1559,plain,
( ~ cC64(iV3102)
| cC216(iV3102) ),
inference(sor,[status(thm)],[616,237]),
[iquote('0:SoR:616.0,237.2')] ).
cnf(1561,plain,
cC216(iV3102),
inference(ssi,[status(thm)],[1559,4,2,885,926,932,956,1554]),
[iquote('1:SSi:1559.0,4.0,2.0,885.0,926.0,932.0,956.0,1554.0')] ).
cnf(1562,plain,
( ~ cC30(iV3102)
| ~ cC46(iV3102)
| xsd_string(skc5) ),
inference(mrr,[status(thm)],[1555,1561]),
[iquote('1:MRR:1555.2,1561.0')] ).
cnf(1563,plain,
( ~ cC30(iV3102)
| ~ cC46(iV3102)
| xsd_integer(skc5) ),
inference(mrr,[status(thm)],[1556,1561]),
[iquote('1:MRR:1556.2,1561.0')] ).
cnf(1574,plain,
( ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC46(iV3102)
| ~ cC30(iV3102) ),
inference(ems,[status(thm)],[81,1563,1562]),
[iquote('1:EmS:81.0,81.1,1563.2,1562.2')] ).
cnf(1575,plain,
( ~ cC46(iV3102)
| ~ cC30(iV3102) ),
inference(obv,[status(thm),theory(equality)],[1574]),
[iquote('1:Obv:1574.1')] ).
cnf(1577,plain,
( ~ cTEST(iV3102)
| ~ cC30(iV3102) ),
inference(res,[status(thm),theory(equality)],[80,1575]),
[iquote('1:Res:80.1,1575.0')] ).
cnf(1578,plain,
~ cC30(iV3102),
inference(ssi,[status(thm)],[1577,4,2,885,926,932,956,1554,1561]),
[iquote('1:SSi:1577.0,4.0,2.0,885.0,926.0,932.0,956.0,1554.0,1561.0')] ).
cnf(1579,plain,
~ cC46(iV3102),
inference(res,[status(thm),theory(equality)],[64,1578]),
[iquote('1:Res:64.1,1578.0')] ).
cnf(1580,plain,
$false,
inference(ssi,[status(thm)],[1579,80,4,2,885,926,932,956,1554,1561]),
[iquote('1:SSi:1579.0,80.0,4.0,2.0,885.0,926.0,932.0,956.0,1554.0,1561.1')] ).
cnf(1581,plain,
~ cC10(iV3102),
inference(spt,[spt(split,[position(sa)])],[1580,885]),
[iquote('1:Spt:1580.0,870.1,885.0')] ).
cnf(1582,plain,
cC6(skf102(u)),
inference(spt,[spt(split,[position(s2)])],[870]),
[iquote('1:Spt:1580.0,870.0')] ).
cnf(1583,plain,
cC8(iV3102),
inference(mrr,[status(thm)],[868,1581]),
[iquote('1:MRR:868.0,1581.0')] ).
cnf(1590,plain,
cC64(iV3102),
inference(ssi,[status(thm)],[1552,4,2,926,932,956]),
[iquote('0:SSi:1552.0,4.0,2.0,926.0,932.0,956.0')] ).
cnf(1591,plain,
cC216(iV3102),
inference(ssi,[status(thm)],[1559,79,59,4,2,926,932,956]),
[iquote('0:SSi:1559.0,79.0,59.0,4.0,2.0,926.0,932.1,956.1')] ).
cnf(1592,plain,
( ~ cC30(iV3102)
| ~ cC46(iV3102)
| xsd_integer(skc5) ),
inference(mrr,[status(thm)],[958,1590,1591]),
[iquote('0:MRR:958.0,958.3,1590.0,1591.0')] ).
cnf(1593,plain,
( ~ cC30(iV3102)
| ~ cC46(iV3102)
| xsd_string(skc5) ),
inference(mrr,[status(thm)],[957,1590,1591]),
[iquote('0:MRR:957.0,957.3,1590.0,1591.0')] ).
cnf(1603,plain,
( ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC46(iV3102)
| ~ cC30(iV3102) ),
inference(ems,[status(thm)],[81,1592,1593]),
[iquote('0:EmS:81.0,81.1,1592.2,1593.2')] ).
cnf(1605,plain,
( ~ cC46(iV3102)
| ~ cC30(iV3102) ),
inference(obv,[status(thm),theory(equality)],[1603]),
[iquote('0:Obv:1603.1')] ).
cnf(1615,plain,
( ~ cTEST(iV3102)
| ~ cC30(iV3102) ),
inference(res,[status(thm),theory(equality)],[80,1605]),
[iquote('0:Res:80.1,1605.0')] ).
cnf(1616,plain,
~ cC30(iV3102),
inference(ssi,[status(thm)],[1615,4,2,926,932,956,1583,1590,1591]),
[iquote('1:SSi:1615.0,4.0,2.0,926.0,932.0,956.0,1583.0,1590.0,1591.0')] ).
cnf(1617,plain,
~ cC46(iV3102),
inference(res,[status(thm),theory(equality)],[64,1616]),
[iquote('1:Res:64.1,1616.0')] ).
cnf(1618,plain,
$false,
inference(ssi,[status(thm)],[1617,80,4,2,926,932,956,1583,1590,1591]),
[iquote('1:SSi:1617.0,80.0,4.0,2.0,926.0,932.0,956.0,1583.0,1590.0,1591.1')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : KRS149+1 : TPTP v8.1.0. Released v3.1.0.
% 0.11/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n024.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 : 600
% 0.12/0.33 % DateTime : Tue Jun 7 08:59:04 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.75/0.97
% 0.75/0.97 SPASS V 3.9
% 0.75/0.97 SPASS beiseite: Proof found.
% 0.75/0.97 % SZS status Theorem
% 0.75/0.97 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.75/0.97 SPASS derived 961 clauses, backtracked 19 clauses, performed 4 splits and kept 1018 clauses.
% 0.75/0.97 SPASS allocated 103156 KBytes.
% 0.75/0.97 SPASS spent 0:00:00.62 on the problem.
% 0.75/0.97 0:00:00.04 for the input.
% 0.75/0.97 0:00:00.34 for the FLOTTER CNF translation.
% 0.75/0.97 0:00:00.01 for inferences.
% 0.75/0.97 0:00:00.00 for the backtracking.
% 0.75/0.97 0:00:00.16 for the reduction.
% 0.75/0.97
% 0.75/0.97
% 0.75/0.97 Here is a proof with depth 3, length 77 :
% 0.75/0.97 % SZS output start Refutation
% See solution above
% 0.75/0.97 Formulae used in the proof : axiom_0 axiom_108 axiom_112 axiom_114 axiom_115 axiom_116 axiom_121 axiom_122 axiom_123 axiom_124 axiom_1 axiom_64 axiom_65 axiom_78 axiom_107 axiom_2 axiom_24 axiom_69 axiom_77 axiom_87 axiom_96 axiom_88 axiom_110 the_axiom
% 0.75/0.97
%------------------------------------------------------------------------------