%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : PRO004+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n017.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 50.92s 51.12s
% Output : Refutation 52.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 38
% Syntax : Number of clauses : 139 ( 48 unt; 22 nHn; 139 RR)
% Number of literals : 345 ( 0 equ; 197 neg)
% Maximal clause size : 8 ( 2 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 15 ( 14 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('PRO004+2.p',unknown),
[] ).
cnf(3,axiom,
atomic(tptp3),
file('PRO004+2.p',unknown),
[] ).
cnf(5,axiom,
atomic(tptp1),
file('PRO004+2.p',unknown),
[] ).
cnf(6,axiom,
occurrence_of(skc1,tptp0),
file('PRO004+2.p',unknown),
[] ).
cnf(8,axiom,
~ atomic(tptp0),
file('PRO004+2.p',unknown),
[] ).
cnf(10,axiom,
occurrence_of(skf32(u),tptp4),
file('PRO004+2.p',unknown),
[] ).
cnf(11,axiom,
occurrence_of(skf31(u),tptp3),
file('PRO004+2.p',unknown),
[] ).
cnf(15,axiom,
~ equal(tptp1,tptp3),
file('PRO004+2.p',unknown),
[] ).
cnf(19,axiom,
( ~ precedes(u,v)
| legal(v) ),
file('PRO004+2.p',unknown),
[] ).
cnf(20,axiom,
( ~ root(u,v)
| legal(u) ),
file('PRO004+2.p',unknown),
[] ).
cnf(23,axiom,
( ~ occurrence_of(u,v)
| activity(v) ),
file('PRO004+2.p',unknown),
[] ).
cnf(24,axiom,
( ~ occurrence_of(u,v)
| activity_occurrence(u) ),
file('PRO004+2.p',unknown),
[] ).
cnf(29,axiom,
( ~ root_occ(u,v)
| subactivity_occurrence(u,v) ),
file('PRO004+2.p',unknown),
[] ).
cnf(30,axiom,
( ~ leaf_occ(u,v)
| subactivity_occurrence(u,v) ),
file('PRO004+2.p',unknown),
[] ).
cnf(31,axiom,
( ~ activity_occurrence(u)
| occurrence_of(u,skf23(u)) ),
file('PRO004+2.p',unknown),
[] ).
cnf(32,axiom,
( ~ min_precedes(u,v,w)
| precedes(u,v) ),
file('PRO004+2.p',unknown),
[] ).
cnf(34,axiom,
( ~ occurrence_of(u,tptp0)
| root_occ(skf32(u),u) ),
file('PRO004+2.p',unknown),
[] ).
cnf(35,axiom,
( ~ occurrence_of(u,tptp0)
| leaf_occ(skf31(u),u) ),
file('PRO004+2.p',unknown),
[] ).
cnf(36,axiom,
( ~ next_subocc(u,v,w)
| min_precedes(u,v,w) ),
file('PRO004+2.p',unknown),
[] ).
cnf(39,axiom,
( ~ root_occ(u,v)
| root(u,skf18(u,w)) ),
file('PRO004+2.p',unknown),
[] ).
cnf(42,axiom,
( ~ arboreal(u)
| ~ occurrence_of(u,v)
| atomic(v) ),
file('PRO004+2.p',unknown),
[] ).
cnf(43,axiom,
( ~ atomic(u)
| ~ occurrence_of(v,u)
| arboreal(v) ),
file('PRO004+2.p',unknown),
[] ).
cnf(55,axiom,
( ~ occurrence_of(u,tptp0)
| next_subocc(skf32(u),skf31(u),tptp0) ),
file('PRO004+2.p',unknown),
[] ).
cnf(57,axiom,
( ~ occurrence_of(u,v)
| ~ occurrence_of(u,w)
| equal(w,v) ),
file('PRO004+2.p',unknown),
[] ).
cnf(60,axiom,
( ~ min_precedes(u,v,w)
| occurrence_of(skf25(v,u,w),w) ),
file('PRO004+2.p',unknown),
[] ).
cnf(61,axiom,
( ~ min_precedes(u,v,w)
| subactivity_occurrence(u,skf25(v,u,x)) ),
file('PRO004+2.p',unknown),
[] ).
cnf(62,axiom,
( ~ min_precedes(u,v,w)
| subactivity_occurrence(v,skf25(v,x,y)) ),
file('PRO004+2.p',unknown),
[] ).
cnf(65,axiom,
( ~ occurrence_of(u,v)
| atomic(v)
| root(skf30(u,v),v) ),
file('PRO004+2.p',unknown),
[] ).
cnf(66,axiom,
( ~ occurrence_of(u,v)
| atomic(v)
| subactivity_occurrence(skf30(u,w),u) ),
file('PRO004+2.p',unknown),
[] ).
cnf(69,axiom,
( ~ root_occ(u,v)
| ~ occurrence_of(v,w)
| ~ min_precedes(x,u,w) ),
file('PRO004+2.p',unknown),
[] ).
cnf(70,axiom,
( ~ leaf_occ(u,v)
| ~ occurrence_of(v,w)
| ~ min_precedes(u,x,w) ),
file('PRO004+2.p',unknown),
[] ).
cnf(74,axiom,
( ~ root_occ(u,v)
| ~ root_occ(w,v)
| ~ occurrence_of(v,x)
| equal(w,u) ),
file('PRO004+2.p',unknown),
[] ).
cnf(75,axiom,
( ~ next_subocc(u,v,w)
| ~ min_precedes(x,v,w)
| ~ min_precedes(u,x,w) ),
file('PRO004+2.p',unknown),
[] ).
cnf(76,axiom,
( ~ subactivity_occurrence(u,v)
| ~ root(u,w)
| ~ occurrence_of(v,w)
| root_occ(u,v) ),
file('PRO004+2.p',unknown),
[] ).
cnf(82,axiom,
( ~ arboreal(u)
| ~ subactivity_occurrence(u,v)
| ~ occurrence_of(v,tptp0)
| root_occ(u,v)
| leaf_occ(u,v) ),
file('PRO004+2.p',unknown),
[] ).
cnf(83,axiom,
( ~ arboreal(u)
| ~ subactivity_occurrence(u,v)
| ~ occurrence_of(v,tptp0)
| leaf_occ(u,v)
| occurrence_of(skf33(w),tptp1) ),
file('PRO004+2.p',unknown),
[] ).
cnf(84,axiom,
( ~ arboreal(u)
| ~ subactivity_occurrence(u,v)
| ~ occurrence_of(v,tptp0)
| leaf_occ(u,v)
| next_subocc(u,skf33(u),tptp0) ),
file('PRO004+2.p',unknown),
[] ).
cnf(85,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('PRO004+2.p',unknown),
[] ).
cnf(86,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(87,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(89,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(90,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(92,plain,
( root(skf30(skc1,tptp0),tptp0)
| atomic(tptp0) ),
inference(res,[status(thm),theory(equality)],[6,65]),
[iquote('0:Res:6.0,65.0')] ).
cnf(93,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(94,plain,
( ~ arboreal(skc1)
| atomic(tptp0) ),
inference(res,[status(thm),theory(equality)],[6,42]),
[iquote('0:Res:6.0,42.1')] ).
cnf(96,plain,
activity_occurrence(skc1),
inference(res,[status(thm),theory(equality)],[6,24]),
[iquote('0:Res:6.0,24.0')] ).
cnf(97,plain,
next_subocc(skf32(skc1),skf31(skc1),tptp0),
inference(res,[status(thm),theory(equality)],[6,55]),
[iquote('0:Res:6.0,55.0')] ).
cnf(98,plain,
root_occ(skf32(skc1),skc1),
inference(res,[status(thm),theory(equality)],[6,34]),
[iquote('0:Res:6.0,34.0')] ).
cnf(101,plain,
( ~ atomic(tptp0)
| arboreal(skc1) ),
inference(res,[status(thm),theory(equality)],[6,43]),
[iquote('0:Res:6.0,43.1')] ).
cnf(108,plain,
~ arboreal(skc1),
inference(mrr,[status(thm)],[94,8]),
[iquote('0:MRR:94.1,8.0')] ).
cnf(109,plain,
~ atomic(tptp0),
inference(mrr,[status(thm)],[101,108]),
[iquote('0:MRR:101.1,108.0')] ).
cnf(110,plain,
root(skf30(skc1,tptp0),tptp0),
inference(mrr,[status(thm)],[92,109]),
[iquote('0:MRR:92.1,109.0')] ).
cnf(111,plain,
subactivity_occurrence(skf30(skc1,u),skc1),
inference(mrr,[status(thm)],[93,109]),
[iquote('0:MRR:93.1,109.0')] ).
cnf(114,plain,
( ~ arboreal(u)
| ~ subactivity_occurrence(u,v)
| ~ occurrence_of(v,tptp0)
| leaf_occ(u,v) ),
inference(spt,[spt(split,[position(s1)])],[83]),
[iquote('1:Spt:83.0,83.1,83.2,83.3')] ).
cnf(120,plain,
activity(tptp3),
inference(res,[status(thm),theory(equality)],[11,23]),
[iquote('0:Res:11.0,23.0')] ).
cnf(121,plain,
activity(tptp4),
inference(res,[status(thm),theory(equality)],[10,23]),
[iquote('0:Res:10.0,23.0')] ).
cnf(126,plain,
activity_occurrence(skf31(u)),
inference(res,[status(thm),theory(equality)],[11,24]),
[iquote('0:Res:11.0,24.0')] ).
cnf(127,plain,
activity_occurrence(skf32(u)),
inference(res,[status(thm),theory(equality)],[10,24]),
[iquote('0:Res:10.0,24.0')] ).
cnf(155,plain,
( ~ atomic(tptp3)
| arboreal(skf31(u)) ),
inference(res,[status(thm),theory(equality)],[11,43]),
[iquote('0:Res:11.0,43.1')] ).
cnf(156,plain,
( ~ atomic(tptp4)
| arboreal(skf32(u)) ),
inference(res,[status(thm),theory(equality)],[10,43]),
[iquote('0:Res:10.0,43.1')] ).
cnf(158,plain,
arboreal(skf31(u)),
inference(ssi,[status(thm)],[155,3,120]),
[iquote('0:SSi:155.0,3.0,120.0')] ).
cnf(159,plain,
arboreal(skf32(u)),
inference(ssi,[status(thm)],[156,2,121]),
[iquote('0:SSi:156.0,2.0,121.0')] ).
cnf(208,plain,
root(skf32(skc1),skf18(skf32(skc1),u)),
inference(res,[status(thm),theory(equality)],[98,39]),
[iquote('0:Res:98.0,39.0')] ).
cnf(212,plain,
legal(skf32(skc1)),
inference(res,[status(thm),theory(equality)],[208,20]),
[iquote('0:Res:208.0,20.0')] ).
cnf(218,plain,
min_precedes(skf32(skc1),skf31(skc1),tptp0),
inference(res,[status(thm),theory(equality)],[97,36]),
[iquote('0:Res:97.0,36.0')] ).
cnf(222,plain,
~ leaf_occ(skf32(skc1),skc1),
inference(res,[status(thm),theory(equality)],[218,90]),
[iquote('0:Res:218.0,90.1')] ).
cnf(225,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(352,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(354,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(361,plain,
( ~ occurrence_of(u,v)
| equal(v,skf23(u)) ),
inference(mrr,[status(thm)],[354,24]),
[iquote('0:MRR:354.0,24.1')] ).
cnf(363,plain,
( ~ activity_occurrence(skf31(u))
| equal(skf23(skf31(u)),tptp3) ),
inference(res,[status(thm),theory(equality)],[31,352]),
[iquote('0:Res:31.1,352.0')] ).
cnf(367,plain,
equal(skf23(skf31(u)),tptp3),
inference(ssi,[status(thm)],[363,126,158]),
[iquote('0:SSi:363.0,126.0,158.0')] ).
cnf(496,plain,
subactivity_occurrence(skf32(skc1),skf25(skf31(skc1),skf32(skc1),u)),
inference(res,[status(thm),theory(equality)],[218,61]),
[iquote('0:Res:218.0,61.0')] ).
cnf(497,plain,
( ~ occurrence_of(u,tptp0)
| subactivity_occurrence(skf32(u),skf25(skf31(u),skf32(u),v)) ),
inference(res,[status(thm),theory(equality)],[225,61]),
[iquote('0:Res:225.1,61.0')] ).
cnf(500,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)],[496,114]),
[iquote('1:Res:496.0,114.1')] ).
cnf(501,plain,
( ~ occurrence_of(skf25(skf31(skc1),skf32(skc1),u),tptp0)
| leaf_occ(skf32(skc1),skf25(skf31(skc1),skf32(skc1),u)) ),
inference(ssi,[status(thm)],[500,212,127,96,159]),
[iquote('1:SSi:500.0,212.0,127.0,96.0,159.0,96.0')] ).
cnf(551,plain,
( ~ leaf_occ(skf32(skc1),u)
| ~ occurrence_of(u,tptp0) ),
inference(res,[status(thm),theory(equality)],[218,70]),
[iquote('0:Res:218.0,70.2')] ).
cnf(552,plain,
( ~ occurrence_of(u,tptp0)
| ~ leaf_occ(skf32(u),v)
| ~ occurrence_of(v,tptp0) ),
inference(res,[status(thm),theory(equality)],[225,70]),
[iquote('0:Res:225.1,70.2')] ).
cnf(553,plain,
~ occurrence_of(skf25(skf31(skc1),skf32(skc1),u),tptp0),
inference(mrr,[status(thm)],[501,551]),
[iquote('1:MRR:501.1,551.0')] ).
cnf(554,plain,
~ min_precedes(skf32(skc1),skf31(skc1),tptp0),
inference(res,[status(thm),theory(equality)],[60,553]),
[iquote('1:Res:60.1,553.0')] ).
cnf(555,plain,
$false,
inference(mrr,[status(thm)],[554,218]),
[iquote('1:MRR:554.0,218.0')] ).
cnf(556,plain,
occurrence_of(skf33(u),tptp1),
inference(spt,[spt(split,[position(s2)])],[83]),
[iquote('1:Spt:555.0,83.4')] ).
cnf(557,plain,
equal(skf23(skf33(u)),tptp1),
inference(res,[status(thm),theory(equality)],[556,361]),
[iquote('1:Res:556.0,361.0')] ).
cnf(561,plain,
activity_occurrence(skf33(u)),
inference(res,[status(thm),theory(equality)],[556,24]),
[iquote('1:Res:556.0,24.0')] ).
cnf(563,plain,
( ~ atomic(tptp1)
| arboreal(skf33(u)) ),
inference(res,[status(thm),theory(equality)],[556,43]),
[iquote('1:Res:556.0,43.1')] ).
cnf(564,plain,
arboreal(skf33(u)),
inference(ssi,[status(thm)],[563,5]),
[iquote('1:SSi:563.0,5.0')] ).
cnf(699,plain,
( ~ root(skf30(skc1,u),tptp0)
| root_occ(skf30(skc1,u),skc1) ),
inference(res,[status(thm),theory(equality)],[111,87]),
[iquote('0:Res:111.0,87.0')] ).
cnf(700,plain,
root_occ(skf30(skc1,tptp0),skc1),
inference(res,[status(thm),theory(equality)],[110,699]),
[iquote('0:Res:110.0,699.0')] ).
cnf(749,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(753,plain,
( ~ root_occ(u,skc1)
| equal(u,skf32(skc1)) ),
inference(res,[status(thm),theory(equality)],[98,86]),
[iquote('0:Res:98.0,86.0')] ).
cnf(758,plain,
equal(skf30(skc1,tptp0),skf32(skc1)),
inference(res,[status(thm),theory(equality)],[700,753]),
[iquote('0:Res:700.0,753.0')] ).
cnf(780,plain,
subactivity_occurrence(skf32(skc1),skc1),
inference(spr,[status(thm),theory(equality)],[758,111]),
[iquote('0:SpR:758.0,111.0')] ).
cnf(901,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)],[780,84]),
[iquote('0:Res:780.0,84.1')] ).
cnf(902,plain,
( ~ occurrence_of(skc1,tptp0)
| leaf_occ(skf32(skc1),skc1)
| next_subocc(skf32(skc1),skf33(skf32(skc1)),tptp0) ),
inference(ssi,[status(thm)],[901,212,127,96,159]),
[iquote('0:SSi:901.0,212.0,127.0,96.0,159.0,96.0')] ).
cnf(903,plain,
next_subocc(skf32(skc1),skf33(skf32(skc1)),tptp0),
inference(mrr,[status(thm)],[902,6,222]),
[iquote('0:MRR:902.0,902.1,6.0,222.0')] ).
cnf(906,plain,
min_precedes(skf32(skc1),skf33(skf32(skc1)),tptp0),
inference(res,[status(thm),theory(equality)],[903,36]),
[iquote('0:Res:903.0,36.0')] ).
cnf(912,plain,
subactivity_occurrence(skf33(skf32(skc1)),skf25(skf33(skf32(skc1)),u,v)),
inference(res,[status(thm),theory(equality)],[906,62]),
[iquote('0:Res:906.0,62.0')] ).
cnf(913,plain,
subactivity_occurrence(skf32(skc1),skf25(skf33(skf32(skc1)),skf32(skc1),u)),
inference(res,[status(thm),theory(equality)],[906,61]),
[iquote('0:Res:906.0,61.0')] ).
cnf(919,plain,
precedes(skf32(skc1),skf33(skf32(skc1))),
inference(res,[status(thm),theory(equality)],[906,32]),
[iquote('0:Res:906.0,32.0')] ).
cnf(925,plain,
( ~ root_occ(skf33(skf32(skc1)),u)
| ~ occurrence_of(u,tptp0) ),
inference(res,[status(thm),theory(equality)],[906,69]),
[iquote('0:Res:906.0,69.2')] ).
cnf(927,plain,
legal(skf33(skf32(skc1))),
inference(res,[status(thm),theory(equality)],[919,19]),
[iquote('0:Res:919.0,19.0')] ).
cnf(928,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,85]),
[iquote('0:Res:30.1,85.2')] ).
cnf(929,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,85]),
[iquote('0:Res:29.1,85.2')] ).
cnf(935,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)],[929,69]),
[iquote('0:MRR:929.7,69.2')] ).
cnf(936,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)],[928,70]),
[iquote('0:MRR:928.6,70.2')] ).
cnf(976,plain,
( ~ arboreal(skf33(skf32(skc1)))
| ~ occurrence_of(skf25(skf33(skf32(skc1)),u,v),tptp0)
| root_occ(skf33(skf32(skc1)),skf25(skf33(skf32(skc1)),u,v))
| leaf_occ(skf33(skf32(skc1)),skf25(skf33(skf32(skc1)),u,v)) ),
inference(res,[status(thm),theory(equality)],[912,82]),
[iquote('0:Res:912.0,82.1')] ).
cnf(983,plain,
( ~ occurrence_of(skf25(skf33(skf32(skc1)),u,v),tptp0)
| root_occ(skf33(skf32(skc1)),skf25(skf33(skf32(skc1)),u,v))
| leaf_occ(skf33(skf32(skc1)),skf25(skf33(skf32(skc1)),u,v)) ),
inference(ssi,[status(thm)],[976,927,561,212,127,96,159,564]),
[iquote('1:SSi:976.0,927.0,561.0,212.0,127.0,96.0,159.0,96.0,564.0,212.0,127.0,96.0,159.0,96.0')] ).
cnf(984,plain,
( ~ occurrence_of(skf25(skf33(skf32(skc1)),u,v),tptp0)
| leaf_occ(skf33(skf32(skc1)),skf25(skf33(skf32(skc1)),u,v)) ),
inference(mrr,[status(thm)],[983,925]),
[iquote('1:MRR:983.1,925.0')] ).
cnf(1285,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)],[497,84]),
[iquote('0:Res:497.1,84.1')] ).
cnf(1292,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)],[1285,127,159]),
[iquote('0:SSi:1285.0,127.0,159.0')] ).
cnf(1293,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)],[1292,552]),
[iquote('0:MRR:1292.2,552.1')] ).
cnf(2530,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,935]),
[iquote('0:Res:34.1,935.2')] ).
cnf(2532,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)],[2530,127,159]),
[iquote('0:SSi:2530.0,127.0,159.0')] ).
cnf(2550,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,936]),
[iquote('0:Res:35.1,936.2')] ).
cnf(2554,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)],[2550,126,158]),
[iquote('0:SSi:2550.0,126.0,158.0')] ).
cnf(5382,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)],[2532,89]),
[iquote('0:Res:2532.5,89.1')] ).
cnf(5411,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)],[5382]),
[iquote('0:Obv:5382.1')] ).
cnf(5512,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)],[2554,749]),
[iquote('0:Res:2554.5,749.1')] ).
cnf(5532,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)],[5512]),
[iquote('0:Obv:5512.2')] ).
cnf(11171,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)],[913,5411]),
[iquote('0:Res:913.0,5411.2')] ).
cnf(11193,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)],[11171,212,127,96,159]),
[iquote('0:SSi:11171.0,212.0,127.0,96.0,159.0,96.0')] ).
cnf(11194,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)],[11193,98]),
[iquote('0:MRR:11193.1,98.0')] ).
cnf(12022,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,1293]),
[iquote('0:Res:60.1,1293.1')] ).
cnf(12023,plain,
( ~ occurrence_of(u,tptp0)
| next_subocc(skf32(u),skf33(skf32(u)),tptp0) ),
inference(mrr,[status(thm)],[12022,225]),
[iquote('0:MRR:12022.0,225.1')] ).
cnf(12027,plain,
( ~ occurrence_of(u,tptp0)
| min_precedes(skf32(u),skf33(skf32(u)),tptp0) ),
inference(res,[status(thm),theory(equality)],[12023,36]),
[iquote('0:Res:12023.1,36.0')] ).
cnf(18230,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)],[12027,5532]),
[iquote('0:Res:12027.1,5532.3')] ).
cnf(18246,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)],[18230]),
[iquote('0:Obv:18230.1')] ).
cnf(18247,plain,
( ~ subactivity_occurrence(skf33(skf32(u)),u)
| ~ occurrence_of(u,tptp0)
| equal(skf33(skf32(u)),skf31(u)) ),
inference(ssi,[status(thm)],[18246,561,127,159,564]),
[iquote('1:SSi:18246.0,561.0,127.0,159.0,564.0,127.0,159.0')] ).
cnf(18542,plain,
( ~ leaf_occ(skf33(skf32(u)),u)
| ~ occurrence_of(u,tptp0)
| equal(skf33(skf32(u)),skf31(u)) ),
inference(res,[status(thm),theory(equality)],[30,18247]),
[iquote('1:Res:30.1,18247.0')] ).
cnf(41069,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,11194]),
[iquote('0:Res:60.1,11194.0')] ).
cnf(41070,plain,
equal(skf32(skf25(skf33(skf32(skc1)),skf32(skc1),tptp0)),skf32(skc1)),
inference(mrr,[status(thm)],[41069,906]),
[iquote('0:MRR:41069.0,906.0')] ).
cnf(41196,plain,
( ~ leaf_occ(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)],[41070,18542]),
[iquote('1:SpL:41070.0,18542.0')] ).
cnf(41274,plain,
( ~ leaf_occ(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)],[41070,41196]),
[iquote('1:Rew:41070.0,41196.2')] ).
cnf(41275,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)],[41274,984]),
[iquote('1:MRR:41274.0,984.1')] ).
cnf(50233,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,41275]),
[iquote('1:Res:60.1,41275.0')] ).
cnf(50234,plain,
equal(skf31(skf25(skf33(skf32(skc1)),skf32(skc1),tptp0)),skf33(skf32(skc1))),
inference(mrr,[status(thm)],[50233,906]),
[iquote('1:MRR:50233.0,906.0')] ).
cnf(50271,plain,
equal(skf23(skf33(skf32(skc1))),tptp3),
inference(spr,[status(thm),theory(equality)],[50234,367]),
[iquote('1:SpR:50234.0,367.0')] ).
cnf(50405,plain,
equal(tptp1,tptp3),
inference(rew,[status(thm),theory(equality)],[557,50271]),
[iquote('1:Rew:557.0,50271.0')] ).
cnf(50406,plain,
$false,
inference(mrr,[status(thm)],[50405,15]),
[iquote('1:MRR:50405.0,15.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : PRO004+2 : TPTP v8.1.0. Released v4.0.0.
% 0.06/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n017.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 : Mon Jun 13 01:29:37 EDT 2022
% 0.12/0.33 % CPUTime :
% 50.92/51.12
% 50.92/51.12 SPASS V 3.9
% 50.92/51.12 SPASS beiseite: Proof found.
% 50.92/51.12 % SZS status Theorem
% 50.92/51.12 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 50.92/51.12 SPASS derived 39751 clauses, backtracked 3664 clauses, performed 66 splits and kept 17136 clauses.
% 50.92/51.12 SPASS allocated 149367 KBytes.
% 50.92/51.12 SPASS spent 0:0:50.73 on the problem.
% 50.92/51.12 0:00:00.03 for the input.
% 50.92/51.12 0:00:00.08 for the FLOTTER CNF translation.
% 50.92/51.12 0:00:01.06 for inferences.
% 50.92/51.12 0:00:02.65 for the backtracking.
% 50.92/51.12 0:0:46.25 for the reduction.
% 50.92/51.12
% 50.92/51.12
% 50.92/51.12 Here is a proof with depth 13, length 139 :
% 50.92/51.12 % SZS output start Refutation
% See solution above
% 52.59/52.80 Formulae used in the proof : sos_35 sos_36 sos_38 goals sos_34 sos_32 sos_42 sos_08 sos_12 sos_29 sos_10 sos_11 sos_18 sos_06 sos_04 sos_13 sos_22 sos_24 sos_30 sos_20 sos_21 sos_02 sos_46 sos_47 sos_28
% 52.59/52.80
%------------------------------------------------------------------------------