%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : PRO001+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% 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:10 EDT 2022
% Result : Theorem 274.24s 274.53s
% Output : Refutation 274.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 33
% Syntax : Number of clauses : 74 ( 40 unt; 7 nHn; 74 RR)
% Number of literals : 130 ( 11 equ; 60 neg)
% Maximal clause size : 8 ( 1 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 1 prp; 0-5 aty)
% Number of functors : 17 ( 17 usr; 6 con; 0-5 aty)
% Number of variables : 101 ( 22 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(3,axiom,
( ~ occurrence_of(X,Y)
| ~ root_occ(Z,X)
| ~ root_occ(U,X)
| Z = U ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_02) ).
cnf(6,axiom,
( ~ next_subocc(X,Y,Z)
| ~ min_precedes(X,U,Z)
| ~ min_precedes(U,Y,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_04) ).
cnf(10,axiom,
( ~ next_subocc(X,Y,Z)
| arboreal(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_05) ).
cnf(20,axiom,
( root_occ(X,Y)
| ~ occurrence_of(Y,Z)
| ~ subactivity_occurrence(X,Y)
| ~ root(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_10) ).
cnf(22,axiom,
( ~ leaf_occ(X,Y)
| subactivity_occurrence(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_11) ).
cnf(25,axiom,
( ~ root(X,Y)
| legal(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_12) ).
cnf(37,axiom,
( ~ legal(X)
| arboreal(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_17) ).
cnf(39,axiom,
( ~ activity_occurrence(X)
| occurrence_of(X,'SKOLEMAAAV7'(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_18) ).
cnf(40,axiom,
( ~ subactivity_occurrence(X,Y)
| activity_occurrence(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_19) ).
cnf(43,axiom,
( ~ occurrence_of(X,Y)
| ~ leaf_occ(Z,X)
| ~ min_precedes(Z,U,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_21) ).
cnf(44,axiom,
( ~ occurrence_of(X,Y)
| ~ occurrence_of(X,Z)
| Y = Z ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_22) ).
cnf(47,axiom,
( ~ min_precedes(X,Y,Z)
| occurrence_of('SKOLEMAAAV9'(Z,X,Y),Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_24) ).
cnf(48,axiom,
( ~ min_precedes(X,Y,Z)
| subactivity_occurrence(X,'SKOLEMAAAV9'(Z,X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_24) ).
cnf(49,axiom,
( ~ min_precedes(X,Y,Z)
| subactivity_occurrence(Y,'SKOLEMAAAV9'(Z,X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_24) ).
cnf(58,axiom,
( ~ occurrence_of(X,Y)
| ~ arboreal(Z)
| ~ arboreal(U)
| ~ subactivity_occurrence(Z,X)
| ~ subactivity_occurrence(U,X)
| min_precedes(Z,U,Y)
| min_precedes(U,Z,Y)
| Z = U ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_28) ).
cnf(61,axiom,
( ~ occurrence_of(X,Y)
| atomic(Y)
| root('SKOLEMAAAV14'(Y,X),Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_30) ).
cnf(62,axiom,
( ~ occurrence_of(X,Y)
| atomic(Y)
| subactivity_occurrence('SKOLEMAAAV14'(Y,X),X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_30) ).
cnf(65,axiom,
( ~ occurrence_of(X,tptp0)
| root_occ('SKOLEMAAAV15'(X),X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_32) ).
cnf(66,axiom,
( ~ occurrence_of(X,tptp0)
| occurrence_of('SKOLEMAAAV16'(X),tptp3)
| occurrence_of('SKOLEMAAAV16'(X),tptp2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_32) ).
cnf(67,axiom,
( ~ occurrence_of(X,tptp0)
| leaf_occ('SKOLEMAAAV16'(X),X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_32) ).
cnf(68,axiom,
( ~ occurrence_of(X,tptp0)
| next_subocc('SKOLEMAAAV15'(X),'SKOLEMAAAV16'(X),tptp0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_32) ).
cnf(86,axiom,
( ~ send_message(X,Y,Z,U,V)
| X != tptp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_46) ).
cnf(87,axiom,
( ~ send_message(X,Y,Z,U,V)
| X != tptp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_46) ).
cnf(88,axiom,
( ~ send_message(X,Y,Z,U,V)
| ~ occurrence_of(W,X)
| min_precedes(U,W,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_47) ).
cnf(90,axiom,
( ~ transmit_message(X,Y,Z,U,V)
| ~ atomic(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_48) ).
cnf(95,axiom,
( ~ transmit_message(X,Y,Z,U,V)
| ~ occurrence_of(W,X)
| send_message('SKOLEMAAAV17'(Y,Z,U,V,W),Y,Z,U,V) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_51) ).
cnf(96,axiom,
( ~ transmit_message(X,Y,Z,U,V)
| ~ occurrence_of(W,X)
| occurrence_of('SKOLEMAAAV18'(Y,Z,U,V,W),'SKOLEMAAAV17'(Y,Z,U,V,W)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_51) ).
cnf(97,axiom,
( ~ transmit_message(X,Y,Z,U,V)
| ~ occurrence_of(W,X)
| root_occ('SKOLEMAAAV18'(Y,Z,U,V,W),W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_51) ).
cnf(101,axiom,
( ~ tptp1(X,Y,Z)
| root(Z,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_52) ).
cnf(102,axiom,
( ~ tptp1(X,Y,Z)
| ~ occurrence_of(U,X)
| transmit_message('SKOLEMAAAV19'(Z,Y,U),'SKOLEMAAAV20'(Z,Y,U),'SKOLEMAAAV21'(Z,Y,U),Z,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_53) ).
cnf(103,axiom,
( ~ tptp1(X,Y,Z)
| ~ occurrence_of(U,X)
| occurrence_of('SKOLEMAAAV22'(Z,Y,U),'SKOLEMAAAV19'(Z,Y,U)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_53) ).
cnf(106,negated_conjecture,
tptp1('SKOLEMAAAV23',tptp0,'SKOLEMAAAV24'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
cnf(107,negated_conjecture,
occurrence_of('SKOLEMAAAV25','SKOLEMAAAV23'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
cnf(120,plain,
root('SKOLEMAAAV24',tptp0),
inference('HYPERRESOLVE',[status(thm)],[101,106]) ).
cnf(133,plain,
occurrence_of('SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),
inference('HYPERRESOLVE',[status(thm)],[103,106,107]) ).
cnf(134,plain,
transmit_message('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV20'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV21'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV24',tptp0),
inference('HYPERRESOLVE',[status(thm)],[102,106,107]) ).
cnf(198,plain,
( atomic('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'))
| subactivity_occurrence('SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')) ),
inference('HYPERRESOLVE',[status(thm)],[62,133]) ).
cnf(199,plain,
( atomic('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'))
| root('SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),'SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')) ),
inference('HYPERRESOLVE',[status(thm)],[61,133]) ).
cnf(308,plain,
~ atomic('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),
inference('UR-RESOLVE',[status(thm)],[90,134]) ).
cnf(309,plain,
subactivity_occurrence('SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),
inference('REWRITE',[status(thm)],[198,308]) ).
cnf(310,plain,
root('SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),'SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),
inference('REWRITE',[status(thm)],[199,308]) ).
cnf(313,plain,
root_occ('SKOLEMAAAV18'('SKOLEMAAAV20'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV21'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV24',tptp0,'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),
inference('HYPERRESOLVE',[status(thm)],[97,134,133]) ).
cnf(314,plain,
send_message('SKOLEMAAAV17'('SKOLEMAAAV20'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV21'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV24',tptp0,'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),'SKOLEMAAAV20'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV21'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV24',tptp0),
inference('HYPERRESOLVE',[status(thm)],[95,134,133]) ).
cnf(315,plain,
occurrence_of('SKOLEMAAAV18'('SKOLEMAAAV20'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV21'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV24',tptp0,'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),'SKOLEMAAAV17'('SKOLEMAAAV20'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV21'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV24',tptp0,'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'))),
inference('HYPERRESOLVE',[status(thm)],[96,134,133]) ).
cnf(433,plain,
activity_occurrence('SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'))),
inference('HYPERRESOLVE',[status(thm)],[40,309]) ).
cnf(435,plain,
occurrence_of('SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),'SKOLEMAAAV7'('SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')))),
inference('HYPERRESOLVE',[status(thm)],[39,433]) ).
cnf(436,plain,
legal('SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'))),
inference('HYPERRESOLVE',[status(thm)],[25,310]) ).
cnf(437,plain,
root_occ('SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),
inference('HYPERRESOLVE',[status(thm)],[20,310,133,309]) ).
cnf(442,plain,
arboreal('SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'))),
inference('HYPERRESOLVE',[status(thm)],[37,436]) ).
cnf(1089,plain,
'SKOLEMAAAV18'('SKOLEMAAAV20'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV21'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV24',tptp0,'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')) = 'SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),
inference('HYPERRESOLVE',[status(thm)],[3,313,133,437]) ).
cnf(1090,plain,
occurrence_of('SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),'SKOLEMAAAV17'('SKOLEMAAAV20'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV21'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV24',tptp0,'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'))),
inference('REWRITE',[status(thm)],[315,1089,theory(equality)]) ).
cnf(3831,plain,
'SKOLEMAAAV17'('SKOLEMAAAV20'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV21'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV24',tptp0,'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')) = 'SKOLEMAAAV7'('SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'))),
inference('HYPERRESOLVE',[status(thm)],[44,1090,435]) ).
cnf(3832,plain,
send_message('SKOLEMAAAV7'('SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'))),'SKOLEMAAAV20'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV21'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV24',tptp0),
inference('REWRITE',[status(thm)],[314,3831,theory(equality)]) ).
cnf(3834,plain,
'SKOLEMAAAV7'('SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'))) != tptp2,
inference('UR-RESOLVE',[status(thm)],[87,3832]) ).
cnf(3835,plain,
'SKOLEMAAAV7'('SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'))) != tptp3,
inference('UR-RESOLVE',[status(thm)],[86,3832]) ).
cnf(3837,plain,
min_precedes('SKOLEMAAAV24','SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),tptp0),
inference('HYPERRESOLVE',[status(thm)],[88,3832,435]) ).
cnf(3838,plain,
~ occurrence_of('SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),tptp2),
inference('UR-RESOLVE',[status(thm)],[44,3834,435]) ).
cnf(3839,plain,
~ occurrence_of('SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),tptp3),
inference('UR-RESOLVE',[status(thm)],[44,3835,435]) ).
cnf(4020,plain,
subactivity_occurrence('SKOLEMAAAV24','SKOLEMAAAV9'(tptp0,'SKOLEMAAAV24','SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')))),
inference('HYPERRESOLVE',[status(thm)],[48,3837]) ).
cnf(4021,plain,
occurrence_of('SKOLEMAAAV9'(tptp0,'SKOLEMAAAV24','SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'))),tptp0),
inference('HYPERRESOLVE',[status(thm)],[47,3837]) ).
cnf(4023,plain,
subactivity_occurrence('SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),'SKOLEMAAAV9'(tptp0,'SKOLEMAAAV24','SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')))),
inference('HYPERRESOLVE',[status(thm)],[49,3837]) ).
cnf(4564,plain,
root_occ('SKOLEMAAAV24','SKOLEMAAAV9'(tptp0,'SKOLEMAAAV24','SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')))),
inference('HYPERRESOLVE',[status(thm)],[20,4021,4020,120]) ).
cnf(4571,plain,
leaf_occ('SKOLEMAAAV16'('SKOLEMAAAV9'(tptp0,'SKOLEMAAAV24','SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')))),'SKOLEMAAAV9'(tptp0,'SKOLEMAAAV24','SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')))),
inference('HYPERRESOLVE',[status(thm)],[67,4021]) ).
cnf(4572,plain,
root_occ('SKOLEMAAAV15'('SKOLEMAAAV9'(tptp0,'SKOLEMAAAV24','SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')))),'SKOLEMAAAV9'(tptp0,'SKOLEMAAAV24','SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')))),
inference('HYPERRESOLVE',[status(thm)],[65,4021]) ).
cnf(4574,plain,
next_subocc('SKOLEMAAAV15'('SKOLEMAAAV9'(tptp0,'SKOLEMAAAV24','SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')))),'SKOLEMAAAV16'('SKOLEMAAAV9'(tptp0,'SKOLEMAAAV24','SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')))),tptp0),
inference('HYPERRESOLVE',[status(thm)],[68,4021]) ).
cnf(4575,plain,
( occurrence_of('SKOLEMAAAV16'('SKOLEMAAAV9'(tptp0,'SKOLEMAAAV24','SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')))),tptp3)
| occurrence_of('SKOLEMAAAV16'('SKOLEMAAAV9'(tptp0,'SKOLEMAAAV24','SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')))),tptp2) ),
inference('HYPERRESOLVE',[status(thm)],[66,4021]) ).
cnf(10152,plain,
~ min_precedes('SKOLEMAAAV16'('SKOLEMAAAV9'(tptp0,'SKOLEMAAAV24','SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')))),X,tptp0),
inference('UR-RESOLVE',[status(thm)],[43,4571,4021]) ).
cnf(10153,plain,
subactivity_occurrence('SKOLEMAAAV16'('SKOLEMAAAV9'(tptp0,'SKOLEMAAAV24','SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')))),'SKOLEMAAAV9'(tptp0,'SKOLEMAAAV24','SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')))),
inference('HYPERRESOLVE',[status(thm)],[22,4571]) ).
cnf(10161,plain,
'SKOLEMAAAV15'('SKOLEMAAAV9'(tptp0,'SKOLEMAAAV24','SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')))) = 'SKOLEMAAAV24',
inference('HYPERRESOLVE',[status(thm)],[3,4572,4021,4564]) ).
cnf(10162,plain,
next_subocc('SKOLEMAAAV24','SKOLEMAAAV16'('SKOLEMAAAV9'(tptp0,'SKOLEMAAAV24','SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')))),tptp0),
inference('REWRITE',[status(thm)],[4574,10161,theory(equality)]) ).
cnf(10163,plain,
arboreal('SKOLEMAAAV16'('SKOLEMAAAV9'(tptp0,'SKOLEMAAAV24','SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'))))),
inference('HYPERRESOLVE',[status(thm)],[10,10162]) ).
cnf(10165,plain,
~ min_precedes('SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),'SKOLEMAAAV16'('SKOLEMAAAV9'(tptp0,'SKOLEMAAAV24','SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')))),tptp0),
inference('UR-RESOLVE',[status(thm)],[6,10162,3837]) ).
cnf(12810,plain,
'SKOLEMAAAV16'('SKOLEMAAAV9'(tptp0,'SKOLEMAAAV24','SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')))) = 'SKOLEMAAAV14'('SKOLEMAAAV19'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25'),'SKOLEMAAAV22'('SKOLEMAAAV24',tptp0,'SKOLEMAAAV25')),
inference('UR-RESOLVE',[status(thm)],[58,10153,4021,10163,442,4023,10152,10165]) ).
cnf(12812,plain,
$false,
inference('REWRITE',[status(thm)],[4575,3838,3839,12810,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : PRO001+2 : TPTP v8.1.0. Released v4.0.0.
% 0.08/0.13 % Command : run-snark %s %d
% 0.13/0.34 % Computer : n010.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:54:55 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.19/0.46 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.47 *
% 0.19/0.47 *
% 0.19/0.47 #<PACKAGE "SNARK-USER">
% 0.19/0.47 *
% 0.19/0.47 SNARK-TPTP-OPTIONS
% 0.19/0.47 *
% 0.19/0.47 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.19/0.47 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.19/0.47 (USE-FACTORING :POS)
% 0.19/0.47 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.19/0.47 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.19/0.47 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.19/0.47 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.19/0.47 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.19/0.47 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.19/0.47 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.19/0.47 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.19/0.47 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.19/0.47 (DECLARE-TPTP-SYMBOLS2))
% 0.19/0.47 *
% 0.19/0.47 "."
% 0.19/0.47 *
% 0.19/0.47 ; Begin refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-13T01:54:55
% 0.19/0.47 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n010.cluster.edu at 2022-06-13T01:54:55
% 274.24/274.53
% 274.24/274.53
% 274.24/274.53 #||
% 274.24/274.53 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 274.24/274.53 % SZS output start Refutation
% See solution above
% 274.34/274.57 ||#
% 274.34/274.57
% 274.34/274.57 ; Summary of computation:
% 274.34/274.57 ; 726272 formulas have been input or derived (from 4734 formulas).
% 274.34/274.57 ; 12812 ( 2%) were retained. Of these,
% 274.34/274.57 ; 6469 (50%) were simplified or subsumed later,
% 274.34/274.57 ; 6343 (50%) are still being kept.
% 274.34/274.57 ;
% 274.34/274.57 ; Run time in seconds excluding printing time:
% 274.34/274.57 ; 0.013 0% Read assertion file (1 call)
% 274.34/274.57 ; 0.004 0% Assert (56 calls)
% 274.34/274.57 ; 3.036 1% Process new row (496,725 calls)
% 274.34/274.57 ; 20.370 7% Resolution (9,466 calls)
% 274.34/274.57 ; 0.082 0% Paramodulation (4,733 calls)
% 274.34/274.57 ; 0.008 0% Factoring (1,816 calls)
% 274.34/274.57 ; 0.678 0% Condensing (325,031 calls)
% 274.34/274.57 ; 228.922 84% Forward subsumption (325,031 calls)
% 274.34/274.57 ; 0.263 0% Backward subsumption (5,832 calls)
% 274.34/274.57 ; 5.739 2% Clause clause subsumption (2,708,399 calls)
% 274.34/274.57 ; 12.694 5% Forward simplification (489,839 calls)
% 274.34/274.57 ; 0.429 0% Backward simplification (12,812 calls)
% 274.34/274.57 ; 0.039 0% Ordering (23,070 calls)
% 274.34/274.57 ; 0.000 0% Sortal reasoning (32 calls)
% 274.34/274.57 ; 0.001 0% Purity testing (1 call)
% 274.34/274.57 ; 1.725 1% Other
% 274.34/274.57 ; 274.003 Total
% 274.34/274.57 ; 274.093 Real time
% 274.34/274.57 ;
% 274.34/274.57 ; Term-hash-array has 10,451 terms in all.
% 274.34/274.57 ; Feature-vector-row-index has 2,446 entries (3,114 at peak, 5,832 added, 3,386 deleted).
% 274.34/274.57 ; Feature-vector-row-index has 23,859 nodes (24,561 at peak, 51,476 added, 27,617 deleted).
% 274.34/274.57 ; Retrieved 8,824,896 possibly forward subsuming rows in 325,031 calls.
% 274.34/274.57 ; Retrieved 2,674 possibly backward subsumed rows in 5,832 calls.
% 274.34/274.57 ; Path-index has 6,536 entries (7,228 at peak, 10,788 added, 4,252 deleted).
% 274.34/274.57 ; Path-index has 38,173 nodes (40,163 at peak, 46,297 added, 8,124 deleted).
% 274.34/274.57 ; Trie-index has 6,536 entries (7,228 at peak, 10,788 added, 4,252 deleted).
% 274.34/274.57 ; Trie-index has 59,035 nodes (66,639 at peak, 97,193 added, 38,158 deleted).
% 274.34/274.57 ; Retrieved 110,733 generalization terms in 2,825,447 calls.
% 274.34/274.57 ; Retrieved 7,015 instance terms in 6,979 calls.
% 274.34/274.57 ; Retrieved 5,436,333 unifiable terms in 2,903,054 calls.
% 274.34/274.57 ;
% 274.34/274.57 ; The agenda of backward simplifiable rows to process has 641 entries:
% 274.34/274.57 ; 641 with value 0
% 274.34/274.57 ; The agenda of rows to process has 5 entries:
% 274.34/274.57 ; 2 with value 41 1 with value 74 1 with value 95
% 274.34/274.57 ; 1 with value 71
% 274.34/274.57 ; The agenda of rows to give has 3445 entries:
% 274.34/274.57 ; 1 with value (4 33) 97 with value (4 56) 7 with value (4 75)
% 274.34/274.57 ; 1 with value (4 37) 39 with value (4 57) 6 with value (4 76)
% 274.34/274.57 ; 83 with value (4 39) 49 with value (4 58) 16 with value (4 77)
% 274.34/274.57 ; 322 with value (4 40) 32 with value (4 59) 5 with value (4 78)
% 274.34/274.57 ; 263 with value (4 41) 28 with value (4 60) 1 with value (4 79)
% 274.34/274.57 ; 291 with value (4 42) 19 with value (4 61) 5 with value (4 80)
% 274.34/274.57 ; 191 with value (4 43) 20 with value (4 62) 5 with value (4 81)
% 274.34/274.57 ; 214 with value (4 44) 17 with value (4 63) 2 with value (4 82)
% 274.34/274.57 ; 197 with value (4 45) 13 with value (4 64) 6 with value (4 83)
% 274.34/274.57 ; 180 with value (4 46) 16 with value (4 65) 5 with value (4 84)
% 274.34/274.57 ; 180 with value (4 47) 15 with value (4 66) 2 with value (4 85)
% 274.34/274.57 ; 159 with value (4 48) 12 with value (4 67) 5 with value (4 86)
% 274.34/274.57 ; 128 with value (4 49) 18 with value (4 68) 4 with value (4 87)
% 274.34/274.57 ; 135 with value (4 50) 8 with value (4 69) 1 with value (4 88)
% 274.34/274.57 ; 164 with value (4 51) 12 with value (4 70) 1 with value (4 92)
% 274.34/274.57 ; 159 with value (4 52) 13 with value (4 71) 2 with value (4 96)
% 274.34/274.57 ; 89 with value (4 53) 4 with value (4 72) 1 with value (4 97)
% 274.34/274.57 ; 113 with value (4 54) 9 with value (4 73) 1 with value (4 98)
% 274.34/274.57 ; 72 with value (4 55) 7 with value (4 74)
% 274.34/274.57 Evaluation took:
% 274.34/274.57 274.096 seconds of real time
% 274.34/274.57 265.07666 seconds of user run time
% 274.34/274.57 8.967738 seconds of system run time
% 274.34/274.57 [Run times include 24.364 seconds GC run time.]
% 274.34/274.57 0 calls to %EVAL
% 274.34/274.57 0 page faults and
% 274.34/274.57 39,055,330,136 bytes consed.
% 274.34/274.57 :PROOF-FOUND
% 274.34/274.57 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-13T01:59:29
% 274.34/274.57 :PROOF-FOUND
% 274.34/274.57 *
%------------------------------------------------------------------------------