%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : PRO004+4 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n006.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 : Mon Jul 18 17:53:43 EDT 2022
% Result : Theorem 1.56s 1.71s
% Output : Refutation 1.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 39
% Syntax : Number of clauses : 119 ( 48 unt; 15 nHn; 119 RR)
% Number of literals : 242 ( 0 equ; 125 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 16 ( 15 usr; 1 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 10 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(2,axiom,
atomic(tptp4),
file('PRO004+4.p',unknown),
[] ).
cnf(3,axiom,
atomic(tptp3),
file('PRO004+4.p',unknown),
[] ).
cnf(5,axiom,
atomic(tptp1),
file('PRO004+4.p',unknown),
[] ).
cnf(6,axiom,
occurrence_of(skc1,tptp0),
file('PRO004+4.p',unknown),
[] ).
cnf(8,axiom,
~ atomic(tptp0),
file('PRO004+4.p',unknown),
[] ).
cnf(10,axiom,
occurrence_of(skf28(u),tptp4),
file('PRO004+4.p',unknown),
[] ).
cnf(11,axiom,
occurrence_of(skf27(u),tptp3),
file('PRO004+4.p',unknown),
[] ).
cnf(15,axiom,
~ equal(tptp1,tptp3),
file('PRO004+4.p',unknown),
[] ).
cnf(19,axiom,
( ~ occurrence_of(u,v)
| activity(v) ),
file('PRO004+4.p',unknown),
[] ).
cnf(20,axiom,
( ~ occurrence_of(u,v)
| activity_occurrence(u) ),
file('PRO004+4.p',unknown),
[] ).
cnf(23,axiom,
( ~ root(u,v)
| legal(u) ),
file('PRO004+4.p',unknown),
[] ).
cnf(24,axiom,
( ~ precedes(u,v)
| legal(v) ),
file('PRO004+4.p',unknown),
[] ).
cnf(25,axiom,
( ~ activity_occurrence(u)
| occurrence_of(u,skf19(u)) ),
file('PRO004+4.p',unknown),
[] ).
cnf(26,axiom,
( ~ leaf_occ(u,v)
| subactivity_occurrence(u,v) ),
file('PRO004+4.p',unknown),
[] ).
cnf(27,axiom,
( ~ root_occ(u,v)
| subactivity_occurrence(u,v) ),
file('PRO004+4.p',unknown),
[] ).
cnf(32,axiom,
( ~ min_precedes(u,v,w)
| precedes(u,v) ),
file('PRO004+4.p',unknown),
[] ).
cnf(33,axiom,
( ~ occurrence_of(u,tptp0)
| root_occ(skf28(u),u) ),
file('PRO004+4.p',unknown),
[] ).
cnf(34,axiom,
( ~ occurrence_of(u,tptp0)
| leaf_occ(skf27(u),u) ),
file('PRO004+4.p',unknown),
[] ).
cnf(39,axiom,
( ~ leaf(u,v)
| ~ min_precedes(u,w,v) ),
file('PRO004+4.p',unknown),
[] ).
cnf(40,axiom,
( ~ arboreal(u)
| ~ occurrence_of(u,v)
| atomic(v) ),
file('PRO004+4.p',unknown),
[] ).
cnf(41,axiom,
( ~ atomic(u)
| ~ occurrence_of(v,u)
| arboreal(v) ),
file('PRO004+4.p',unknown),
[] ).
cnf(42,axiom,
( ~ leaf_occ(u,v)
| occurrence_of(v,skf23(u,v)) ),
file('PRO004+4.p',unknown),
[] ).
cnf(43,axiom,
( ~ leaf_occ(u,v)
| leaf(u,skf23(u,w)) ),
file('PRO004+4.p',unknown),
[] ).
cnf(45,axiom,
( ~ root_occ(u,v)
| root(u,skf24(u,w)) ),
file('PRO004+4.p',unknown),
[] ).
cnf(47,axiom,
( ~ next_subocc(u,v,w)
| min_precedes(u,v,w) ),
file('PRO004+4.p',unknown),
[] ).
cnf(50,axiom,
( ~ occurrence_of(u,tptp0)
| next_subocc(skf28(u),skf27(u),tptp0) ),
file('PRO004+4.p',unknown),
[] ).
cnf(53,axiom,
( ~ min_precedes(u,v,w)
| occurrence_of(skf17(v,u,w),w) ),
file('PRO004+4.p',unknown),
[] ).
cnf(55,axiom,
( ~ min_precedes(u,v,w)
| subactivity_occurrence(v,skf17(v,x,y)) ),
file('PRO004+4.p',unknown),
[] ).
cnf(56,axiom,
( ~ leaf(u,v)
| atomic(v)
| occurrence_of(skf18(u,v),v) ),
file('PRO004+4.p',unknown),
[] ).
cnf(57,axiom,
( ~ leaf(u,v)
| atomic(v)
| leaf_occ(u,skf18(u,w)) ),
file('PRO004+4.p',unknown),
[] ).
cnf(58,axiom,
( ~ occurrence_of(u,v)
| ~ occurrence_of(u,w)
| equal(w,v) ),
file('PRO004+4.p',unknown),
[] ).
cnf(59,axiom,
( ~ min_precedes(u,v,w)
| min_precedes(skf25(w,v),v,w) ),
file('PRO004+4.p',unknown),
[] ).
cnf(61,axiom,
( ~ leaf_occ(u,v)
| ~ occurrence_of(v,w)
| ~ min_precedes(u,x,w) ),
file('PRO004+4.p',unknown),
[] ).
cnf(62,axiom,
( ~ root_occ(u,v)
| ~ occurrence_of(v,w)
| ~ min_precedes(x,u,w) ),
file('PRO004+4.p',unknown),
[] ).
cnf(66,axiom,
( ~ min_precedes(u,v,w)
| leaf(v,w)
| min_precedes(v,skf22(w,v),w) ),
file('PRO004+4.p',unknown),
[] ).
cnf(76,axiom,
( ~ arboreal(u)
| ~ subactivity_occurrence(u,v)
| ~ occurrence_of(v,tptp0)
| root_occ(u,v)
| leaf_occ(u,v) ),
file('PRO004+4.p',unknown),
[] ).
cnf(78,axiom,
( ~ arboreal(u)
| ~ subactivity_occurrence(u,v)
| ~ occurrence_of(v,tptp0)
| leaf_occ(u,v)
| occurrence_of(skf29(w),tptp1) ),
file('PRO004+4.p',unknown),
[] ).
cnf(79,axiom,
( ~ arboreal(u)
| ~ subactivity_occurrence(u,v)
| ~ occurrence_of(v,tptp0)
| leaf_occ(u,v)
| next_subocc(u,skf29(u),tptp0) ),
file('PRO004+4.p',unknown),
[] ).
cnf(80,axiom,
( ~ arboreal(u)
| ~ occurrence_of(v,w)
| ~ subactivity_occurrence(u,v)
| ~ leaf_occ(x,v)
| equal(x,u)
| min_precedes(u,x,w) ),
file('PRO004+4.p',unknown),
[] ).
cnf(87,plain,
( ~ leaf_occ(u,skc1)
| ~ min_precedes(u,v,tptp0) ),
inference(res,[status(thm),theory(equality)],[6,61]),
[iquote('0:Res:6.0,61.0')] ).
cnf(92,plain,
( ~ arboreal(skc1)
| atomic(tptp0) ),
inference(res,[status(thm),theory(equality)],[6,40]),
[iquote('0:Res:6.0,40.1')] ).
cnf(94,plain,
activity_occurrence(skc1),
inference(res,[status(thm),theory(equality)],[6,20]),
[iquote('0:Res:6.0,20.0')] ).
cnf(95,plain,
next_subocc(skf28(skc1),skf27(skc1),tptp0),
inference(res,[status(thm),theory(equality)],[6,50]),
[iquote('0:Res:6.0,50.0')] ).
cnf(96,plain,
root_occ(skf28(skc1),skc1),
inference(res,[status(thm),theory(equality)],[6,33]),
[iquote('0:Res:6.0,33.0')] ).
cnf(99,plain,
( ~ atomic(tptp0)
| arboreal(skc1) ),
inference(res,[status(thm),theory(equality)],[6,41]),
[iquote('0:Res:6.0,41.1')] ).
cnf(108,plain,
~ arboreal(skc1),
inference(mrr,[status(thm)],[92,8]),
[iquote('0:MRR:92.1,8.0')] ).
cnf(109,plain,
~ atomic(tptp0),
inference(mrr,[status(thm)],[99,108]),
[iquote('0:MRR:99.1,108.0')] ).
cnf(114,plain,
( ~ arboreal(u)
| ~ subactivity_occurrence(u,v)
| ~ occurrence_of(v,tptp0)
| leaf_occ(u,v) ),
inference(spt,[spt(split,[position(s1)])],[78]),
[iquote('1:Spt:78.0,78.1,78.2,78.3')] ).
cnf(118,plain,
activity(tptp3),
inference(res,[status(thm),theory(equality)],[11,19]),
[iquote('0:Res:11.0,19.0')] ).
cnf(119,plain,
activity(tptp4),
inference(res,[status(thm),theory(equality)],[10,19]),
[iquote('0:Res:10.0,19.0')] ).
cnf(124,plain,
activity_occurrence(skf27(u)),
inference(res,[status(thm),theory(equality)],[11,20]),
[iquote('0:Res:11.0,20.0')] ).
cnf(125,plain,
activity_occurrence(skf28(u)),
inference(res,[status(thm),theory(equality)],[10,20]),
[iquote('0:Res:10.0,20.0')] ).
cnf(134,plain,
subactivity_occurrence(skf28(skc1),skc1),
inference(res,[status(thm),theory(equality)],[96,27]),
[iquote('0:Res:96.0,27.0')] ).
cnf(144,plain,
( ~ occurrence_of(u,tptp0)
| subactivity_occurrence(skf28(u),u) ),
inference(res,[status(thm),theory(equality)],[33,27]),
[iquote('0:Res:33.1,27.0')] ).
cnf(156,plain,
( ~ atomic(tptp3)
| arboreal(skf27(u)) ),
inference(res,[status(thm),theory(equality)],[11,41]),
[iquote('0:Res:11.0,41.1')] ).
cnf(157,plain,
( ~ atomic(tptp4)
| arboreal(skf28(u)) ),
inference(res,[status(thm),theory(equality)],[10,41]),
[iquote('0:Res:10.0,41.1')] ).
cnf(159,plain,
arboreal(skf27(u)),
inference(ssi,[status(thm)],[156,3,118]),
[iquote('0:SSi:156.0,3.0,118.0')] ).
cnf(160,plain,
arboreal(skf28(u)),
inference(ssi,[status(thm)],[157,2,119]),
[iquote('0:SSi:157.0,2.0,119.0')] ).
cnf(185,plain,
( ~ leaf_occ(u,v)
| activity_occurrence(v) ),
inference(res,[status(thm),theory(equality)],[42,20]),
[iquote('0:Res:42.1,20.0')] ).
cnf(212,plain,
root(skf28(skc1),skf24(skf28(skc1),u)),
inference(res,[status(thm),theory(equality)],[96,45]),
[iquote('0:Res:96.0,45.0')] ).
cnf(216,plain,
legal(skf28(skc1)),
inference(res,[status(thm),theory(equality)],[212,23]),
[iquote('0:Res:212.0,23.0')] ).
cnf(222,plain,
min_precedes(skf28(skc1),skf27(skc1),tptp0),
inference(res,[status(thm),theory(equality)],[95,47]),
[iquote('0:Res:95.0,47.0')] ).
cnf(226,plain,
~ leaf_occ(skf28(skc1),skc1),
inference(res,[status(thm),theory(equality)],[222,87]),
[iquote('0:Res:222.0,87.1')] ).
cnf(233,plain,
( ~ arboreal(skf28(skc1))
| ~ subactivity_occurrence(skf28(skc1),skc1)
| ~ occurrence_of(skc1,tptp0) ),
inference(res,[status(thm),theory(equality)],[114,226]),
[iquote('1:Res:114.3,226.0')] ).
cnf(237,plain,
( ~ subactivity_occurrence(skf28(skc1),skc1)
| ~ occurrence_of(skc1,tptp0) ),
inference(ssi,[status(thm)],[233,216,125,94,160]),
[iquote('1:SSi:233.0,216.0,125.0,94.0,160.0,94.0')] ).
cnf(238,plain,
$false,
inference(mrr,[status(thm)],[237,144,6]),
[iquote('1:MRR:237.0,237.1,144.1,6.0')] ).
cnf(239,plain,
occurrence_of(skf29(u),tptp1),
inference(spt,[spt(split,[position(s2)])],[78]),
[iquote('1:Spt:238.0,78.4')] ).
cnf(241,plain,
activity_occurrence(skf29(u)),
inference(res,[status(thm),theory(equality)],[239,20]),
[iquote('1:Res:239.0,20.0')] ).
cnf(243,plain,
( ~ atomic(tptp1)
| arboreal(skf29(u)) ),
inference(res,[status(thm),theory(equality)],[239,41]),
[iquote('1:Res:239.0,41.1')] ).
cnf(244,plain,
arboreal(skf29(u)),
inference(ssi,[status(thm)],[243,5]),
[iquote('1:SSi:243.0,5.0')] ).
cnf(284,plain,
( ~ occurrence_of(skf27(u),v)
| equal(v,tptp3) ),
inference(res,[status(thm),theory(equality)],[11,58]),
[iquote('0:Res:11.0,58.0')] ).
cnf(286,plain,
( ~ activity_occurrence(u)
| ~ occurrence_of(u,v)
| equal(v,skf19(u)) ),
inference(res,[status(thm),theory(equality)],[25,58]),
[iquote('0:Res:25.1,58.0')] ).
cnf(290,plain,
( ~ occurrence_of(skf29(u),v)
| equal(v,tptp1) ),
inference(res,[status(thm),theory(equality)],[239,58]),
[iquote('1:Res:239.0,58.0')] ).
cnf(292,plain,
( ~ occurrence_of(u,v)
| equal(v,skf19(u)) ),
inference(mrr,[status(thm)],[286,20]),
[iquote('0:MRR:286.0,20.1')] ).
cnf(294,plain,
( ~ activity_occurrence(skf27(u))
| equal(skf19(skf27(u)),tptp3) ),
inference(res,[status(thm),theory(equality)],[25,284]),
[iquote('0:Res:25.1,284.0')] ).
cnf(298,plain,
equal(skf19(skf27(u)),tptp3),
inference(ssi,[status(thm)],[294,124,159]),
[iquote('0:SSi:294.0,124.0,159.0')] ).
cnf(332,plain,
( ~ activity_occurrence(skf29(u))
| equal(skf19(skf29(u)),tptp1) ),
inference(res,[status(thm),theory(equality)],[25,290]),
[iquote('1:Res:25.1,290.0')] ).
cnf(337,plain,
equal(skf19(skf29(u)),tptp1),
inference(ssi,[status(thm)],[332,241,244]),
[iquote('1:SSi:332.0,241.0,244.0')] ).
cnf(348,plain,
( ~ leaf_occ(u,v)
| equal(skf23(u,v),skf19(v)) ),
inference(res,[status(thm),theory(equality)],[42,292]),
[iquote('0:Res:42.1,292.0')] ).
cnf(882,plain,
( ~ arboreal(skf28(skc1))
| ~ occurrence_of(skc1,tptp0)
| leaf_occ(skf28(skc1),skc1)
| next_subocc(skf28(skc1),skf29(skf28(skc1)),tptp0) ),
inference(res,[status(thm),theory(equality)],[134,79]),
[iquote('0:Res:134.0,79.1')] ).
cnf(890,plain,
( ~ occurrence_of(skc1,tptp0)
| leaf_occ(skf28(skc1),skc1)
| next_subocc(skf28(skc1),skf29(skf28(skc1)),tptp0) ),
inference(ssi,[status(thm)],[882,216,125,94,160]),
[iquote('0:SSi:882.0,216.0,125.0,94.0,160.0,94.0')] ).
cnf(891,plain,
next_subocc(skf28(skc1),skf29(skf28(skc1)),tptp0),
inference(mrr,[status(thm)],[890,6,226]),
[iquote('0:MRR:890.0,890.1,6.0,226.0')] ).
cnf(899,plain,
min_precedes(skf28(skc1),skf29(skf28(skc1)),tptp0),
inference(res,[status(thm),theory(equality)],[891,47]),
[iquote('0:Res:891.0,47.0')] ).
cnf(903,plain,
( leaf(skf29(skf28(skc1)),tptp0)
| min_precedes(skf29(skf28(skc1)),skf22(tptp0,skf29(skf28(skc1))),tptp0) ),
inference(res,[status(thm),theory(equality)],[899,66]),
[iquote('0:Res:899.0,66.0')] ).
cnf(904,plain,
subactivity_occurrence(skf29(skf28(skc1)),skf17(skf29(skf28(skc1)),u,v)),
inference(res,[status(thm),theory(equality)],[899,55]),
[iquote('0:Res:899.0,55.0')] ).
cnf(907,plain,
min_precedes(skf25(tptp0,skf29(skf28(skc1))),skf29(skf28(skc1)),tptp0),
inference(res,[status(thm),theory(equality)],[899,59]),
[iquote('0:Res:899.0,59.0')] ).
cnf(909,plain,
precedes(skf28(skc1),skf29(skf28(skc1))),
inference(res,[status(thm),theory(equality)],[899,32]),
[iquote('0:Res:899.0,32.0')] ).
cnf(917,plain,
( ~ root_occ(skf29(skf28(skc1)),u)
| ~ occurrence_of(u,tptp0) ),
inference(res,[status(thm),theory(equality)],[899,62]),
[iquote('0:Res:899.0,62.2')] ).
cnf(922,plain,
legal(skf29(skf28(skc1))),
inference(res,[status(thm),theory(equality)],[909,24]),
[iquote('0:Res:909.0,24.0')] ).
cnf(927,plain,
( ~ activity_occurrence(u)
| ~ arboreal(v)
| ~ subactivity_occurrence(v,u)
| ~ leaf_occ(w,u)
| equal(w,v)
| min_precedes(v,w,skf19(u)) ),
inference(res,[status(thm),theory(equality)],[25,80]),
[iquote('0:Res:25.1,80.1')] ).
cnf(933,plain,
( ~ arboreal(u)
| ~ subactivity_occurrence(u,v)
| ~ leaf_occ(w,v)
| equal(w,u)
| min_precedes(u,w,skf19(v)) ),
inference(mrr,[status(thm)],[927,185]),
[iquote('0:MRR:927.0,185.1')] ).
cnf(1568,plain,
( leaf(skf29(skf28(skc1)),tptp0)
| precedes(skf29(skf28(skc1)),skf22(tptp0,skf29(skf28(skc1)))) ),
inference(res,[status(thm),theory(equality)],[903,32]),
[iquote('0:Res:903.1,32.0')] ).
cnf(1576,plain,
( ~ leaf_occ(skf29(skf28(skc1)),u)
| ~ occurrence_of(u,tptp0)
| leaf(skf29(skf28(skc1)),tptp0) ),
inference(res,[status(thm),theory(equality)],[903,61]),
[iquote('0:Res:903.1,61.2')] ).
cnf(1601,plain,
leaf(skf29(skf28(skc1)),tptp0),
inference(spt,[spt(split,[position(s2s1)])],[1568]),
[iquote('2:Spt:1568.0')] ).
cnf(1609,plain,
( atomic(tptp0)
| leaf_occ(skf29(skf28(skc1)),skf18(skf29(skf28(skc1)),u)) ),
inference(res,[status(thm),theory(equality)],[1601,57]),
[iquote('2:Res:1601.0,57.0')] ).
cnf(1612,plain,
leaf_occ(skf29(skf28(skc1)),skf18(skf29(skf28(skc1)),u)),
inference(mrr,[status(thm)],[1609,109]),
[iquote('2:MRR:1609.0,109.0')] ).
cnf(1616,plain,
leaf(skf29(skf28(skc1)),skf23(skf29(skf28(skc1)),u)),
inference(res,[status(thm),theory(equality)],[1612,43]),
[iquote('2:Res:1612.0,43.0')] ).
cnf(1620,plain,
( ~ leaf_occ(skf29(skf28(skc1)),u)
| leaf(skf29(skf28(skc1)),skf19(u)) ),
inference(spr,[status(thm),theory(equality)],[348,1616]),
[iquote('2:SpR:348.1,1616.0')] ).
cnf(1991,plain,
( ~ arboreal(u)
| ~ subactivity_occurrence(u,v)
| ~ leaf_occ(w,v)
| ~ leaf(u,skf19(v))
| equal(w,u) ),
inference(res,[status(thm),theory(equality)],[933,39]),
[iquote('0:Res:933.4,39.1')] ).
cnf(4827,plain,
( ~ arboreal(skf29(skf28(skc1)))
| ~ leaf_occ(skf29(skf28(skc1)),u)
| ~ subactivity_occurrence(skf29(skf28(skc1)),u)
| ~ leaf_occ(v,u)
| equal(v,skf29(skf28(skc1))) ),
inference(res,[status(thm),theory(equality)],[1620,1991]),
[iquote('2:Res:1620.1,1991.3')] ).
cnf(4830,plain,
( ~ leaf_occ(skf29(skf28(skc1)),u)
| ~ subactivity_occurrence(skf29(skf28(skc1)),u)
| ~ leaf_occ(v,u)
| equal(v,skf29(skf28(skc1))) ),
inference(ssi,[status(thm)],[4827,922,241,216,125,94,160,244]),
[iquote('2:SSi:4827.0,922.0,241.0,216.0,125.0,94.0,160.0,94.0,244.0,216.0,125.0,94.0,160.0,94.0')] ).
cnf(4831,plain,
( ~ leaf_occ(skf29(skf28(skc1)),u)
| ~ leaf_occ(v,u)
| equal(v,skf29(skf28(skc1))) ),
inference(mrr,[status(thm)],[4830,26]),
[iquote('2:MRR:4830.1,26.1')] ).
cnf(4856,plain,
( ~ leaf_occ(u,skf18(skf29(skf28(skc1)),v))
| equal(u,skf29(skf28(skc1))) ),
inference(res,[status(thm),theory(equality)],[1612,4831]),
[iquote('2:Res:1612.0,4831.0')] ).
cnf(4876,plain,
( ~ occurrence_of(skf18(skf29(skf28(skc1)),u),tptp0)
| equal(skf27(skf18(skf29(skf28(skc1)),u)),skf29(skf28(skc1))) ),
inference(res,[status(thm),theory(equality)],[34,4856]),
[iquote('2:Res:34.1,4856.0')] ).
cnf(5714,plain,
( ~ leaf(skf29(skf28(skc1)),tptp0)
| atomic(tptp0)
| equal(skf27(skf18(skf29(skf28(skc1)),tptp0)),skf29(skf28(skc1))) ),
inference(res,[status(thm),theory(equality)],[56,4876]),
[iquote('2:Res:56.2,4876.0')] ).
cnf(5715,plain,
equal(skf27(skf18(skf29(skf28(skc1)),tptp0)),skf29(skf28(skc1))),
inference(mrr,[status(thm)],[5714,1601,109]),
[iquote('2:MRR:5714.0,5714.1,1601.0,109.0')] ).
cnf(5723,plain,
equal(skf19(skf29(skf28(skc1))),tptp3),
inference(spr,[status(thm),theory(equality)],[5715,298]),
[iquote('2:SpR:5715.0,298.0')] ).
cnf(5789,plain,
equal(tptp1,tptp3),
inference(rew,[status(thm),theory(equality)],[337,5723]),
[iquote('2:Rew:337.0,5723.0')] ).
cnf(5790,plain,
$false,
inference(mrr,[status(thm)],[5789,15]),
[iquote('2:MRR:5789.0,15.0')] ).
cnf(5818,plain,
~ leaf(skf29(skf28(skc1)),tptp0),
inference(spt,[spt(split,[position(s2sa)])],[5790,1601]),
[iquote('2:Spt:5790.0,1568.0,1601.0')] ).
cnf(5819,plain,
precedes(skf29(skf28(skc1)),skf22(tptp0,skf29(skf28(skc1)))),
inference(spt,[spt(split,[position(s2s2)])],[1568]),
[iquote('2:Spt:5790.0,1568.1')] ).
cnf(5824,plain,
( ~ leaf_occ(skf29(skf28(skc1)),u)
| ~ occurrence_of(u,tptp0) ),
inference(mrr,[status(thm)],[1576,5818]),
[iquote('2:MRR:1576.2,5818.0')] ).
cnf(6014,plain,
( ~ arboreal(skf29(skf28(skc1)))
| ~ subactivity_occurrence(skf29(skf28(skc1)),u)
| ~ occurrence_of(u,tptp0)
| ~ occurrence_of(u,tptp0)
| root_occ(skf29(skf28(skc1)),u) ),
inference(res,[status(thm),theory(equality)],[76,5824]),
[iquote('2:Res:76.4,5824.0')] ).
cnf(6018,plain,
( ~ arboreal(skf29(skf28(skc1)))
| ~ subactivity_occurrence(skf29(skf28(skc1)),u)
| ~ occurrence_of(u,tptp0)
| root_occ(skf29(skf28(skc1)),u) ),
inference(obv,[status(thm),theory(equality)],[6014]),
[iquote('2:Obv:6014.2')] ).
cnf(6019,plain,
( ~ subactivity_occurrence(skf29(skf28(skc1)),u)
| ~ occurrence_of(u,tptp0)
| root_occ(skf29(skf28(skc1)),u) ),
inference(ssi,[status(thm)],[6018,922,241,216,125,94,160,244]),
[iquote('2:SSi:6018.0,922.0,241.0,216.0,125.0,94.0,160.0,94.0,244.0,216.0,125.0,94.0,160.0,94.0')] ).
cnf(6020,plain,
( ~ subactivity_occurrence(skf29(skf28(skc1)),u)
| ~ occurrence_of(u,tptp0) ),
inference(mrr,[status(thm)],[6019,917]),
[iquote('2:MRR:6019.2,917.0')] ).
cnf(6024,plain,
~ occurrence_of(skf17(skf29(skf28(skc1)),u,v),tptp0),
inference(res,[status(thm),theory(equality)],[904,6020]),
[iquote('2:Res:904.0,6020.0')] ).
cnf(6061,plain,
~ min_precedes(u,skf29(skf28(skc1)),tptp0),
inference(res,[status(thm),theory(equality)],[53,6024]),
[iquote('2:Res:53.1,6024.0')] ).
cnf(6062,plain,
$false,
inference(unc,[status(thm)],[6061,907]),
[iquote('2:UnC:6061.0,907.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : PRO004+4 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n006.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Mon Jun 13 01:58:12 EDT 2022
% 0.13/0.34 % CPUTime :
% 1.56/1.71
% 1.56/1.71 SPASS V 3.9
% 1.56/1.71 SPASS beiseite: Proof found.
% 1.56/1.71 % SZS status Theorem
% 1.56/1.71 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.56/1.71 SPASS derived 4850 clauses, backtracked 122 clauses, performed 15 splits and kept 2024 clauses.
% 1.56/1.71 SPASS allocated 103285 KBytes.
% 1.56/1.71 SPASS spent 0:00:01.36 on the problem.
% 1.56/1.71 0:00:00.03 for the input.
% 1.56/1.71 0:00:00.08 for the FLOTTER CNF translation.
% 1.56/1.71 0:00:00.08 for inferences.
% 1.56/1.71 0:00:00.01 for the backtracking.
% 1.56/1.71 0:00:01.10 for the reduction.
% 1.56/1.71
% 1.56/1.71
% 1.56/1.71 Here is a proof with depth 15, length 119 :
% 1.56/1.71 % SZS output start Refutation
% See solution above
% 1.56/1.74 Formulae used in the proof : sos_35 sos_36 sos_38 goals sos_34 sos_32 sos_42 sos_03 sos_17 sos_21 sos_12 sos_18 sos_19 sos_24 sos_15 sos_16 sos_26 sos_06 sos_07 sos_08 sos_23 sos_09 sos_10 sos_46 sos_47 sos_02
% 1.56/1.74
%------------------------------------------------------------------------------