%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : PRO006+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n010.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:44 EDT 2022
% Result : Theorem 53.29s 53.47s
% Output : Refutation 54.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 35
% Syntax : Number of clauses : 129 ( 46 unt; 19 nHn; 129 RR)
% Number of literals : 320 ( 0 equ; 184 neg)
% Maximal clause size : 8 ( 2 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 14 ( 13 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 10 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(2,axiom,
atomic(tptp4),
file('PRO006+2.p',unknown),
[] ).
cnf(3,axiom,
atomic(tptp3),
file('PRO006+2.p',unknown),
[] ).
cnf(5,axiom,
atomic(tptp1),
file('PRO006+2.p',unknown),
[] ).
cnf(6,axiom,
occurrence_of(skc1,tptp0),
file('PRO006+2.p',unknown),
[] ).
cnf(8,axiom,
~ atomic(tptp0),
file('PRO006+2.p',unknown),
[] ).
cnf(10,axiom,
occurrence_of(skf32(u),tptp4),
file('PRO006+2.p',unknown),
[] ).
cnf(11,axiom,
occurrence_of(skf31(u),tptp3),
file('PRO006+2.p',unknown),
[] ).
cnf(15,axiom,
~ equal(tptp1,tptp3),
file('PRO006+2.p',unknown),
[] ).
cnf(20,axiom,
( ~ root(u,v)
| legal(u) ),
file('PRO006+2.p',unknown),
[] ).
cnf(23,axiom,
( ~ occurrence_of(u,v)
| activity(v) ),
file('PRO006+2.p',unknown),
[] ).
cnf(24,axiom,
( ~ occurrence_of(u,v)
| activity_occurrence(u) ),
file('PRO006+2.p',unknown),
[] ).
cnf(29,axiom,
( ~ root_occ(u,v)
| subactivity_occurrence(u,v) ),
file('PRO006+2.p',unknown),
[] ).
cnf(30,axiom,
( ~ leaf_occ(u,v)
| subactivity_occurrence(u,v) ),
file('PRO006+2.p',unknown),
[] ).
cnf(31,axiom,
( ~ activity_occurrence(u)
| occurrence_of(u,skf23(u)) ),
file('PRO006+2.p',unknown),
[] ).
cnf(34,axiom,
( ~ occurrence_of(u,tptp0)
| root_occ(skf32(u),u) ),
file('PRO006+2.p',unknown),
[] ).
cnf(35,axiom,
( ~ occurrence_of(u,tptp0)
| leaf_occ(skf31(u),u) ),
file('PRO006+2.p',unknown),
[] ).
cnf(36,axiom,
( ~ next_subocc(u,v,w)
| min_precedes(u,v,w) ),
file('PRO006+2.p',unknown),
[] ).
cnf(39,axiom,
( ~ root_occ(u,v)
| root(u,skf18(u,w)) ),
file('PRO006+2.p',unknown),
[] ).
cnf(42,axiom,
( ~ arboreal(u)
| ~ occurrence_of(u,v)
| atomic(v) ),
file('PRO006+2.p',unknown),
[] ).
cnf(43,axiom,
( ~ atomic(u)
| ~ occurrence_of(v,u)
| arboreal(v) ),
file('PRO006+2.p',unknown),
[] ).
cnf(55,axiom,
( ~ occurrence_of(u,tptp0)
| next_subocc(skf32(u),skf31(u),tptp0) ),
file('PRO006+2.p',unknown),
[] ).
cnf(57,axiom,
( ~ occurrence_of(u,v)
| ~ occurrence_of(u,w)
| equal(w,v) ),
file('PRO006+2.p',unknown),
[] ).
cnf(60,axiom,
( ~ min_precedes(u,v,w)
| occurrence_of(skf25(v,u,w),w) ),
file('PRO006+2.p',unknown),
[] ).
cnf(61,axiom,
( ~ min_precedes(u,v,w)
| subactivity_occurrence(u,skf25(v,u,x)) ),
file('PRO006+2.p',unknown),
[] ).
cnf(62,axiom,
( ~ min_precedes(u,v,w)
| subactivity_occurrence(v,skf25(v,x,y)) ),
file('PRO006+2.p',unknown),
[] ).
cnf(65,axiom,
( ~ occurrence_of(u,v)
| atomic(v)
| root(skf30(u,v),v) ),
file('PRO006+2.p',unknown),
[] ).
cnf(66,axiom,
( ~ occurrence_of(u,v)
| atomic(v)
| subactivity_occurrence(skf30(u,w),u) ),
file('PRO006+2.p',unknown),
[] ).
cnf(69,axiom,
( ~ root_occ(u,v)
| ~ occurrence_of(v,w)
| ~ min_precedes(x,u,w) ),
file('PRO006+2.p',unknown),
[] ).
cnf(70,axiom,
( ~ leaf_occ(u,v)
| ~ occurrence_of(v,w)
| ~ min_precedes(u,x,w) ),
file('PRO006+2.p',unknown),
[] ).
cnf(74,axiom,
( ~ root_occ(u,v)
| ~ root_occ(w,v)
| ~ occurrence_of(v,x)
| equal(w,u) ),
file('PRO006+2.p',unknown),
[] ).
cnf(75,axiom,
( ~ next_subocc(u,v,w)
| ~ min_precedes(x,v,w)
| ~ min_precedes(u,x,w) ),
file('PRO006+2.p',unknown),
[] ).
cnf(76,axiom,
( ~ subactivity_occurrence(u,v)
| ~ root(u,w)
| ~ occurrence_of(v,w)
| root_occ(u,v) ),
file('PRO006+2.p',unknown),
[] ).
cnf(81,axiom,
( ~ arboreal(u)
| ~ subactivity_occurrence(u,v)
| ~ occurrence_of(v,tptp0)
| leaf_occ(u,v)
| occurrence_of(skf33(w),tptp1) ),
file('PRO006+2.p',unknown),
[] ).
cnf(82,axiom,
( ~ arboreal(u)
| ~ subactivity_occurrence(u,v)
| ~ occurrence_of(v,tptp0)
| leaf_occ(u,v)
| next_subocc(u,skf33(u),tptp0) ),
file('PRO006+2.p',unknown),
[] ).
cnf(83,axiom,
( ~ arboreal(u)
| ~ arboreal(v)
| ~ subactivity_occurrence(u,w)
| ~ occurrence_of(w,x)
| ~ subactivity_occurrence(v,w)
| equal(v,u)
| min_precedes(u,v,x)
| min_precedes(v,u,x) ),
file('PRO006+2.p',unknown),
[] ).
cnf(84,plain,
( ~ root_occ(u,skc1)
| ~ root_occ(v,skc1)
| equal(v,u) ),
inference(res,[status(thm),theory(equality)],[6,74]),
[iquote('0:Res:6.0,74.0')] ).
cnf(85,plain,
( ~ subactivity_occurrence(u,skc1)
| ~ root(u,tptp0)
| root_occ(u,skc1) ),
inference(res,[status(thm),theory(equality)],[6,76]),
[iquote('0:Res:6.0,76.0')] ).
cnf(87,plain,
( ~ root_occ(u,skc1)
| ~ min_precedes(v,u,tptp0) ),
inference(res,[status(thm),theory(equality)],[6,69]),
[iquote('0:Res:6.0,69.0')] ).
cnf(88,plain,
( ~ leaf_occ(u,skc1)
| ~ min_precedes(u,v,tptp0) ),
inference(res,[status(thm),theory(equality)],[6,70]),
[iquote('0:Res:6.0,70.0')] ).
cnf(90,plain,
( root(skf30(skc1,tptp0),tptp0)
| atomic(tptp0) ),
inference(res,[status(thm),theory(equality)],[6,65]),
[iquote('0:Res:6.0,65.0')] ).
cnf(91,plain,
( subactivity_occurrence(skf30(skc1,u),skc1)
| atomic(tptp0) ),
inference(res,[status(thm),theory(equality)],[6,66]),
[iquote('0:Res:6.0,66.0')] ).
cnf(92,plain,
( ~ arboreal(skc1)
| atomic(tptp0) ),
inference(res,[status(thm),theory(equality)],[6,42]),
[iquote('0:Res:6.0,42.1')] ).
cnf(94,plain,
activity_occurrence(skc1),
inference(res,[status(thm),theory(equality)],[6,24]),
[iquote('0:Res:6.0,24.0')] ).
cnf(95,plain,
next_subocc(skf32(skc1),skf31(skc1),tptp0),
inference(res,[status(thm),theory(equality)],[6,55]),
[iquote('0:Res:6.0,55.0')] ).
cnf(96,plain,
root_occ(skf32(skc1),skc1),
inference(res,[status(thm),theory(equality)],[6,34]),
[iquote('0:Res:6.0,34.0')] ).
cnf(99,plain,
( ~ atomic(tptp0)
| arboreal(skc1) ),
inference(res,[status(thm),theory(equality)],[6,43]),
[iquote('0:Res:6.0,43.1')] ).
cnf(105,plain,
~ arboreal(skc1),
inference(mrr,[status(thm)],[92,8]),
[iquote('0:MRR:92.1,8.0')] ).
cnf(106,plain,
~ atomic(tptp0),
inference(mrr,[status(thm)],[99,105]),
[iquote('0:MRR:99.1,105.0')] ).
cnf(107,plain,
root(skf30(skc1,tptp0),tptp0),
inference(mrr,[status(thm)],[90,106]),
[iquote('0:MRR:90.1,106.0')] ).
cnf(108,plain,
subactivity_occurrence(skf30(skc1,u),skc1),
inference(mrr,[status(thm)],[91,106]),
[iquote('0:MRR:91.1,106.0')] ).
cnf(111,plain,
( ~ arboreal(u)
| ~ subactivity_occurrence(u,v)
| ~ occurrence_of(v,tptp0)
| leaf_occ(u,v) ),
inference(spt,[spt(split,[position(s1)])],[81]),
[iquote('1:Spt:81.0,81.1,81.2,81.3')] ).
cnf(117,plain,
activity(tptp3),
inference(res,[status(thm),theory(equality)],[11,23]),
[iquote('0:Res:11.0,23.0')] ).
cnf(118,plain,
activity(tptp4),
inference(res,[status(thm),theory(equality)],[10,23]),
[iquote('0:Res:10.0,23.0')] ).
cnf(123,plain,
activity_occurrence(skf31(u)),
inference(res,[status(thm),theory(equality)],[11,24]),
[iquote('0:Res:11.0,24.0')] ).
cnf(124,plain,
activity_occurrence(skf32(u)),
inference(res,[status(thm),theory(equality)],[10,24]),
[iquote('0:Res:10.0,24.0')] ).
cnf(152,plain,
( ~ atomic(tptp3)
| arboreal(skf31(u)) ),
inference(res,[status(thm),theory(equality)],[11,43]),
[iquote('0:Res:11.0,43.1')] ).
cnf(153,plain,
( ~ atomic(tptp4)
| arboreal(skf32(u)) ),
inference(res,[status(thm),theory(equality)],[10,43]),
[iquote('0:Res:10.0,43.1')] ).
cnf(155,plain,
arboreal(skf31(u)),
inference(ssi,[status(thm)],[152,3,117]),
[iquote('0:SSi:152.0,3.0,117.0')] ).
cnf(156,plain,
arboreal(skf32(u)),
inference(ssi,[status(thm)],[153,2,118]),
[iquote('0:SSi:153.0,2.0,118.0')] ).
cnf(205,plain,
root(skf32(skc1),skf18(skf32(skc1),u)),
inference(res,[status(thm),theory(equality)],[96,39]),
[iquote('0:Res:96.0,39.0')] ).
cnf(209,plain,
legal(skf32(skc1)),
inference(res,[status(thm),theory(equality)],[205,20]),
[iquote('0:Res:205.0,20.0')] ).
cnf(215,plain,
min_precedes(skf32(skc1),skf31(skc1),tptp0),
inference(res,[status(thm),theory(equality)],[95,36]),
[iquote('0:Res:95.0,36.0')] ).
cnf(219,plain,
~ leaf_occ(skf32(skc1),skc1),
inference(res,[status(thm),theory(equality)],[215,88]),
[iquote('0:Res:215.0,88.1')] ).
cnf(222,plain,
( ~ occurrence_of(u,tptp0)
| min_precedes(skf32(u),skf31(u),tptp0) ),
inference(res,[status(thm),theory(equality)],[55,36]),
[iquote('0:Res:55.1,36.0')] ).
cnf(349,plain,
( ~ occurrence_of(skf31(u),v)
| equal(v,tptp3) ),
inference(res,[status(thm),theory(equality)],[11,57]),
[iquote('0:Res:11.0,57.0')] ).
cnf(351,plain,
( ~ activity_occurrence(u)
| ~ occurrence_of(u,v)
| equal(v,skf23(u)) ),
inference(res,[status(thm),theory(equality)],[31,57]),
[iquote('0:Res:31.1,57.0')] ).
cnf(358,plain,
( ~ occurrence_of(u,v)
| equal(v,skf23(u)) ),
inference(mrr,[status(thm)],[351,24]),
[iquote('0:MRR:351.0,24.1')] ).
cnf(360,plain,
( ~ activity_occurrence(skf31(u))
| equal(skf23(skf31(u)),tptp3) ),
inference(res,[status(thm),theory(equality)],[31,349]),
[iquote('0:Res:31.1,349.0')] ).
cnf(364,plain,
equal(skf23(skf31(u)),tptp3),
inference(ssi,[status(thm)],[360,123,155]),
[iquote('0:SSi:360.0,123.0,155.0')] ).
cnf(493,plain,
subactivity_occurrence(skf32(skc1),skf25(skf31(skc1),skf32(skc1),u)),
inference(res,[status(thm),theory(equality)],[215,61]),
[iquote('0:Res:215.0,61.0')] ).
cnf(494,plain,
( ~ occurrence_of(u,tptp0)
| subactivity_occurrence(skf32(u),skf25(skf31(u),skf32(u),v)) ),
inference(res,[status(thm),theory(equality)],[222,61]),
[iquote('0:Res:222.1,61.0')] ).
cnf(497,plain,
( ~ arboreal(skf32(skc1))
| ~ occurrence_of(skf25(skf31(skc1),skf32(skc1),u),tptp0)
| leaf_occ(skf32(skc1),skf25(skf31(skc1),skf32(skc1),u)) ),
inference(res,[status(thm),theory(equality)],[493,111]),
[iquote('1:Res:493.0,111.1')] ).
cnf(498,plain,
( ~ occurrence_of(skf25(skf31(skc1),skf32(skc1),u),tptp0)
| leaf_occ(skf32(skc1),skf25(skf31(skc1),skf32(skc1),u)) ),
inference(ssi,[status(thm)],[497,209,124,94,156]),
[iquote('1:SSi:497.0,209.0,124.0,94.0,156.0,94.0')] ).
cnf(548,plain,
( ~ leaf_occ(skf32(skc1),u)
| ~ occurrence_of(u,tptp0) ),
inference(res,[status(thm),theory(equality)],[215,70]),
[iquote('0:Res:215.0,70.2')] ).
cnf(549,plain,
( ~ occurrence_of(u,tptp0)
| ~ leaf_occ(skf32(u),v)
| ~ occurrence_of(v,tptp0) ),
inference(res,[status(thm),theory(equality)],[222,70]),
[iquote('0:Res:222.1,70.2')] ).
cnf(550,plain,
~ occurrence_of(skf25(skf31(skc1),skf32(skc1),u),tptp0),
inference(mrr,[status(thm)],[498,548]),
[iquote('1:MRR:498.1,548.0')] ).
cnf(551,plain,
~ min_precedes(skf32(skc1),skf31(skc1),tptp0),
inference(res,[status(thm),theory(equality)],[60,550]),
[iquote('1:Res:60.1,550.0')] ).
cnf(552,plain,
$false,
inference(mrr,[status(thm)],[551,215]),
[iquote('1:MRR:551.0,215.0')] ).
cnf(553,plain,
occurrence_of(skf33(u),tptp1),
inference(spt,[spt(split,[position(s2)])],[81]),
[iquote('1:Spt:552.0,81.4')] ).
cnf(554,plain,
equal(skf23(skf33(u)),tptp1),
inference(res,[status(thm),theory(equality)],[553,358]),
[iquote('1:Res:553.0,358.0')] ).
cnf(558,plain,
activity_occurrence(skf33(u)),
inference(res,[status(thm),theory(equality)],[553,24]),
[iquote('1:Res:553.0,24.0')] ).
cnf(560,plain,
( ~ atomic(tptp1)
| arboreal(skf33(u)) ),
inference(res,[status(thm),theory(equality)],[553,43]),
[iquote('1:Res:553.0,43.1')] ).
cnf(561,plain,
arboreal(skf33(u)),
inference(ssi,[status(thm)],[560,5]),
[iquote('1:SSi:560.0,5.0')] ).
cnf(696,plain,
( ~ root(skf30(skc1,u),tptp0)
| root_occ(skf30(skc1,u),skc1) ),
inference(res,[status(thm),theory(equality)],[108,85]),
[iquote('0:Res:108.0,85.0')] ).
cnf(697,plain,
root_occ(skf30(skc1,tptp0),skc1),
inference(res,[status(thm),theory(equality)],[107,696]),
[iquote('0:Res:107.0,696.0')] ).
cnf(746,plain,
( ~ occurrence_of(u,tptp0)
| ~ min_precedes(v,skf31(u),tptp0)
| ~ min_precedes(skf32(u),v,tptp0) ),
inference(res,[status(thm),theory(equality)],[55,75]),
[iquote('0:Res:55.1,75.0')] ).
cnf(750,plain,
( ~ root_occ(u,skc1)
| equal(u,skf32(skc1)) ),
inference(res,[status(thm),theory(equality)],[96,84]),
[iquote('0:Res:96.0,84.0')] ).
cnf(755,plain,
equal(skf30(skc1,tptp0),skf32(skc1)),
inference(res,[status(thm),theory(equality)],[697,750]),
[iquote('0:Res:697.0,750.0')] ).
cnf(777,plain,
subactivity_occurrence(skf32(skc1),skc1),
inference(spr,[status(thm),theory(equality)],[755,108]),
[iquote('0:SpR:755.0,108.0')] ).
cnf(881,plain,
( ~ arboreal(skf32(skc1))
| ~ occurrence_of(skc1,tptp0)
| leaf_occ(skf32(skc1),skc1)
| next_subocc(skf32(skc1),skf33(skf32(skc1)),tptp0) ),
inference(res,[status(thm),theory(equality)],[777,82]),
[iquote('0:Res:777.0,82.1')] ).
cnf(882,plain,
( ~ occurrence_of(skc1,tptp0)
| leaf_occ(skf32(skc1),skc1)
| next_subocc(skf32(skc1),skf33(skf32(skc1)),tptp0) ),
inference(ssi,[status(thm)],[881,209,124,94,156]),
[iquote('0:SSi:881.0,209.0,124.0,94.0,156.0,94.0')] ).
cnf(883,plain,
next_subocc(skf32(skc1),skf33(skf32(skc1)),tptp0),
inference(mrr,[status(thm)],[882,6,219]),
[iquote('0:MRR:882.0,882.1,6.0,219.0')] ).
cnf(887,plain,
min_precedes(skf32(skc1),skf33(skf32(skc1)),tptp0),
inference(res,[status(thm),theory(equality)],[883,36]),
[iquote('0:Res:883.0,36.0')] ).
cnf(893,plain,
subactivity_occurrence(skf33(skf32(skc1)),skf25(skf33(skf32(skc1)),u,v)),
inference(res,[status(thm),theory(equality)],[887,62]),
[iquote('0:Res:887.0,62.0')] ).
cnf(894,plain,
subactivity_occurrence(skf32(skc1),skf25(skf33(skf32(skc1)),skf32(skc1),u)),
inference(res,[status(thm),theory(equality)],[887,61]),
[iquote('0:Res:887.0,61.0')] ).
cnf(909,plain,
( ~ arboreal(u)
| ~ arboreal(v)
| ~ leaf_occ(u,w)
| ~ occurrence_of(w,x)
| ~ subactivity_occurrence(v,w)
| equal(v,u)
| min_precedes(u,v,x)
| min_precedes(v,u,x) ),
inference(res,[status(thm),theory(equality)],[30,83]),
[iquote('0:Res:30.1,83.2')] ).
cnf(910,plain,
( ~ arboreal(u)
| ~ arboreal(v)
| ~ root_occ(u,w)
| ~ occurrence_of(w,x)
| ~ subactivity_occurrence(v,w)
| equal(v,u)
| min_precedes(u,v,x)
| min_precedes(v,u,x) ),
inference(res,[status(thm),theory(equality)],[29,83]),
[iquote('0:Res:29.1,83.2')] ).
cnf(916,plain,
( ~ arboreal(u)
| ~ arboreal(v)
| ~ root_occ(u,w)
| ~ occurrence_of(w,x)
| ~ subactivity_occurrence(v,w)
| equal(v,u)
| min_precedes(u,v,x) ),
inference(mrr,[status(thm)],[910,69]),
[iquote('0:MRR:910.7,69.2')] ).
cnf(917,plain,
( ~ arboreal(u)
| ~ arboreal(v)
| ~ leaf_occ(u,w)
| ~ occurrence_of(w,x)
| ~ subactivity_occurrence(v,w)
| equal(v,u)
| min_precedes(v,u,x) ),
inference(mrr,[status(thm)],[909,70]),
[iquote('0:MRR:909.6,70.2')] ).
cnf(1253,plain,
( ~ arboreal(skf32(u))
| ~ occurrence_of(u,tptp0)
| ~ occurrence_of(skf25(skf31(u),skf32(u),v),tptp0)
| leaf_occ(skf32(u),skf25(skf31(u),skf32(u),v))
| next_subocc(skf32(u),skf33(skf32(u)),tptp0) ),
inference(res,[status(thm),theory(equality)],[494,82]),
[iquote('0:Res:494.1,82.1')] ).
cnf(1259,plain,
( ~ occurrence_of(u,tptp0)
| ~ occurrence_of(skf25(skf31(u),skf32(u),v),tptp0)
| leaf_occ(skf32(u),skf25(skf31(u),skf32(u),v))
| next_subocc(skf32(u),skf33(skf32(u)),tptp0) ),
inference(ssi,[status(thm)],[1253,124,156]),
[iquote('0:SSi:1253.0,124.0,156.0')] ).
cnf(1260,plain,
( ~ occurrence_of(u,tptp0)
| ~ occurrence_of(skf25(skf31(u),skf32(u),v),tptp0)
| next_subocc(skf32(u),skf33(skf32(u)),tptp0) ),
inference(mrr,[status(thm)],[1259,549]),
[iquote('0:MRR:1259.2,549.1')] ).
cnf(2479,plain,
( ~ arboreal(skf32(u))
| ~ arboreal(v)
| ~ occurrence_of(u,tptp0)
| ~ occurrence_of(u,w)
| ~ subactivity_occurrence(v,u)
| equal(v,skf32(u))
| min_precedes(skf32(u),v,w) ),
inference(res,[status(thm),theory(equality)],[34,916]),
[iquote('0:Res:34.1,916.2')] ).
cnf(2481,plain,
( ~ arboreal(u)
| ~ occurrence_of(v,tptp0)
| ~ occurrence_of(v,w)
| ~ subactivity_occurrence(u,v)
| equal(u,skf32(v))
| min_precedes(skf32(v),u,w) ),
inference(ssi,[status(thm)],[2479,124,156]),
[iquote('0:SSi:2479.0,124.0,156.0')] ).
cnf(2499,plain,
( ~ arboreal(skf31(u))
| ~ arboreal(v)
| ~ occurrence_of(u,tptp0)
| ~ occurrence_of(u,w)
| ~ subactivity_occurrence(v,u)
| equal(v,skf31(u))
| min_precedes(v,skf31(u),w) ),
inference(res,[status(thm),theory(equality)],[35,917]),
[iquote('0:Res:35.1,917.2')] ).
cnf(2503,plain,
( ~ arboreal(u)
| ~ occurrence_of(v,tptp0)
| ~ occurrence_of(v,w)
| ~ subactivity_occurrence(u,v)
| equal(u,skf31(v))
| min_precedes(u,skf31(v),w) ),
inference(ssi,[status(thm)],[2499,123,155]),
[iquote('0:SSi:2499.0,123.0,155.0')] ).
cnf(5263,plain,
( ~ arboreal(u)
| ~ occurrence_of(v,tptp0)
| ~ occurrence_of(v,tptp0)
| ~ subactivity_occurrence(u,v)
| ~ root_occ(u,skc1)
| equal(u,skf32(v)) ),
inference(res,[status(thm),theory(equality)],[2481,87]),
[iquote('0:Res:2481.5,87.1')] ).
cnf(5292,plain,
( ~ arboreal(u)
| ~ occurrence_of(v,tptp0)
| ~ subactivity_occurrence(u,v)
| ~ root_occ(u,skc1)
| equal(u,skf32(v)) ),
inference(obv,[status(thm),theory(equality)],[5263]),
[iquote('0:Obv:5263.1')] ).
cnf(5395,plain,
( ~ arboreal(u)
| ~ occurrence_of(v,tptp0)
| ~ occurrence_of(v,tptp0)
| ~ subactivity_occurrence(u,v)
| ~ occurrence_of(v,tptp0)
| ~ min_precedes(skf32(v),u,tptp0)
| equal(u,skf31(v)) ),
inference(res,[status(thm),theory(equality)],[2503,746]),
[iquote('0:Res:2503.5,746.1')] ).
cnf(5415,plain,
( ~ arboreal(u)
| ~ subactivity_occurrence(u,v)
| ~ occurrence_of(v,tptp0)
| ~ min_precedes(skf32(v),u,tptp0)
| equal(u,skf31(v)) ),
inference(obv,[status(thm),theory(equality)],[5395]),
[iquote('0:Obv:5395.2')] ).
cnf(10504,plain,
( ~ arboreal(skf32(skc1))
| ~ occurrence_of(skf25(skf33(skf32(skc1)),skf32(skc1),u),tptp0)
| ~ root_occ(skf32(skc1),skc1)
| equal(skf32(skf25(skf33(skf32(skc1)),skf32(skc1),u)),skf32(skc1)) ),
inference(res,[status(thm),theory(equality)],[894,5292]),
[iquote('0:Res:894.0,5292.2')] ).
cnf(10528,plain,
( ~ occurrence_of(skf25(skf33(skf32(skc1)),skf32(skc1),u),tptp0)
| ~ root_occ(skf32(skc1),skc1)
| equal(skf32(skf25(skf33(skf32(skc1)),skf32(skc1),u)),skf32(skc1)) ),
inference(ssi,[status(thm)],[10504,209,124,94,156]),
[iquote('0:SSi:10504.0,209.0,124.0,94.0,156.0,94.0')] ).
cnf(10529,plain,
( ~ occurrence_of(skf25(skf33(skf32(skc1)),skf32(skc1),u),tptp0)
| equal(skf32(skf25(skf33(skf32(skc1)),skf32(skc1),u)),skf32(skc1)) ),
inference(mrr,[status(thm)],[10528,96]),
[iquote('0:MRR:10528.1,96.0')] ).
cnf(11120,plain,
( ~ min_precedes(skf32(u),skf31(u),tptp0)
| ~ occurrence_of(u,tptp0)
| next_subocc(skf32(u),skf33(skf32(u)),tptp0) ),
inference(res,[status(thm),theory(equality)],[60,1260]),
[iquote('0:Res:60.1,1260.1')] ).
cnf(11121,plain,
( ~ occurrence_of(u,tptp0)
| next_subocc(skf32(u),skf33(skf32(u)),tptp0) ),
inference(mrr,[status(thm)],[11120,222]),
[iquote('0:MRR:11120.0,222.1')] ).
cnf(11125,plain,
( ~ occurrence_of(u,tptp0)
| min_precedes(skf32(u),skf33(skf32(u)),tptp0) ),
inference(res,[status(thm),theory(equality)],[11121,36]),
[iquote('0:Res:11121.1,36.0')] ).
cnf(16832,plain,
( ~ arboreal(skf33(skf32(u)))
| ~ occurrence_of(u,tptp0)
| ~ subactivity_occurrence(skf33(skf32(u)),u)
| ~ occurrence_of(u,tptp0)
| equal(skf33(skf32(u)),skf31(u)) ),
inference(res,[status(thm),theory(equality)],[11125,5415]),
[iquote('0:Res:11125.1,5415.3')] ).
cnf(16846,plain,
( ~ arboreal(skf33(skf32(u)))
| ~ subactivity_occurrence(skf33(skf32(u)),u)
| ~ occurrence_of(u,tptp0)
| equal(skf33(skf32(u)),skf31(u)) ),
inference(obv,[status(thm),theory(equality)],[16832]),
[iquote('0:Obv:16832.1')] ).
cnf(16847,plain,
( ~ subactivity_occurrence(skf33(skf32(u)),u)
| ~ occurrence_of(u,tptp0)
| equal(skf33(skf32(u)),skf31(u)) ),
inference(ssi,[status(thm)],[16846,558,124,156,561]),
[iquote('1:SSi:16846.0,558.0,124.0,156.0,561.0,124.0,156.0')] ).
cnf(39533,plain,
( ~ min_precedes(skf32(skc1),skf33(skf32(skc1)),tptp0)
| equal(skf32(skf25(skf33(skf32(skc1)),skf32(skc1),tptp0)),skf32(skc1)) ),
inference(res,[status(thm),theory(equality)],[60,10529]),
[iquote('0:Res:60.1,10529.0')] ).
cnf(39534,plain,
equal(skf32(skf25(skf33(skf32(skc1)),skf32(skc1),tptp0)),skf32(skc1)),
inference(mrr,[status(thm)],[39533,887]),
[iquote('0:MRR:39533.0,887.0')] ).
cnf(39663,plain,
( ~ subactivity_occurrence(skf33(skf32(skc1)),skf25(skf33(skf32(skc1)),skf32(skc1),tptp0))
| ~ occurrence_of(skf25(skf33(skf32(skc1)),skf32(skc1),tptp0),tptp0)
| equal(skf33(skf32(skf25(skf33(skf32(skc1)),skf32(skc1),tptp0))),skf31(skf25(skf33(skf32(skc1)),skf32(skc1),tptp0))) ),
inference(spl,[status(thm),theory(equality)],[39534,16847]),
[iquote('1:SpL:39534.0,16847.0')] ).
cnf(39745,plain,
( ~ subactivity_occurrence(skf33(skf32(skc1)),skf25(skf33(skf32(skc1)),skf32(skc1),tptp0))
| ~ occurrence_of(skf25(skf33(skf32(skc1)),skf32(skc1),tptp0),tptp0)
| equal(skf31(skf25(skf33(skf32(skc1)),skf32(skc1),tptp0)),skf33(skf32(skc1))) ),
inference(rew,[status(thm),theory(equality)],[39534,39663]),
[iquote('1:Rew:39534.0,39663.2')] ).
cnf(39746,plain,
( ~ occurrence_of(skf25(skf33(skf32(skc1)),skf32(skc1),tptp0),tptp0)
| equal(skf31(skf25(skf33(skf32(skc1)),skf32(skc1),tptp0)),skf33(skf32(skc1))) ),
inference(mrr,[status(thm)],[39745,893]),
[iquote('1:MRR:39745.0,893.0')] ).
cnf(48459,plain,
( ~ min_precedes(skf32(skc1),skf33(skf32(skc1)),tptp0)
| equal(skf31(skf25(skf33(skf32(skc1)),skf32(skc1),tptp0)),skf33(skf32(skc1))) ),
inference(res,[status(thm),theory(equality)],[60,39746]),
[iquote('1:Res:60.1,39746.0')] ).
cnf(48460,plain,
equal(skf31(skf25(skf33(skf32(skc1)),skf32(skc1),tptp0)),skf33(skf32(skc1))),
inference(mrr,[status(thm)],[48459,887]),
[iquote('1:MRR:48459.0,887.0')] ).
cnf(48497,plain,
equal(skf23(skf33(skf32(skc1))),tptp3),
inference(spr,[status(thm),theory(equality)],[48460,364]),
[iquote('1:SpR:48460.0,364.0')] ).
cnf(48630,plain,
equal(tptp1,tptp3),
inference(rew,[status(thm),theory(equality)],[554,48497]),
[iquote('1:Rew:554.0,48497.0')] ).
cnf(48631,plain,
$false,
inference(mrr,[status(thm)],[48630,15]),
[iquote('1:MRR:48630.0,15.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : PRO006+2 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.13 % Command : run_spass %d %s
% 0.14/0.34 % Computer : n010.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 600
% 0.14/0.34 % DateTime : Mon Jun 13 03:36:24 EDT 2022
% 0.14/0.34 % CPUTime :
% 53.29/53.47
% 53.29/53.47 SPASS V 3.9
% 53.29/53.47 SPASS beiseite: Proof found.
% 53.29/53.47 % SZS status Theorem
% 53.29/53.47 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 53.29/53.47 SPASS derived 38517 clauses, backtracked 3440 clauses, performed 65 splits and kept 16585 clauses.
% 53.29/53.47 SPASS allocated 148011 KBytes.
% 53.29/53.47 SPASS spent 0:0:53.06 on the problem.
% 53.29/53.47 0:00:00.04 for the input.
% 53.29/53.47 0:00:00.10 for the FLOTTER CNF translation.
% 53.29/53.47 0:00:01.09 for inferences.
% 53.29/53.47 0:00:02.60 for the backtracking.
% 53.29/53.47 0:0:48.51 for the reduction.
% 53.29/53.47
% 53.29/53.47
% 53.29/53.47 Here is a proof with depth 13, length 129 :
% 53.29/53.47 % SZS output start Refutation
% See solution above
% 54.89/55.11 Formulae used in the proof : sos_35 sos_36 sos_38 goals sos_34 sos_32 sos_42 sos_12 sos_29 sos_10 sos_11 sos_18 sos_04 sos_13 sos_22 sos_24 sos_30 sos_20 sos_21 sos_02 sos_45 sos_28
% 54.89/55.11
%------------------------------------------------------------------------------