%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : PRO002+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n021.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:11 EDT 2022
% Result : Theorem 4.11s 4.31s
% Output : Refutation 4.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 40
% Syntax : Number of clauses : 105 ( 64 unt; 8 nHn; 105 RR)
% Number of literals : 163 ( 16 equ; 65 neg)
% Maximal clause size : 8 ( 1 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 1 prp; 0-5 aty)
% Number of functors : 18 ( 18 usr; 7 con; 0-3 aty)
% Number of variables : 102 ( 24 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(4,axiom,
( ~ activity_occurrence(X)
| occurrence_of(X,'SKOLEMAAAV1'(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_01) ).
cnf(5,axiom,
( ~ occurrence_of(X,Y)
| ~ occurrence_of(X,Z)
| Y = Z ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_02) ).
cnf(11,axiom,
( ~ occurrence_of(X,Y)
| arboreal(X)
| ~ atomic(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_07) ).
cnf(12,axiom,
( ~ legal(X)
| arboreal(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_08) ).
cnf(15,axiom,
( ~ precedes(X,Y)
| legal(Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_10) ).
cnf(25,axiom,
( ~ min_precedes(X,Y,Z)
| ~ root(Y,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_14) ).
cnf(26,axiom,
( ~ min_precedes(X,Y,Z)
| precedes(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_15) ).
cnf(27,axiom,
( ~ root(X,Y)
| legal(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_16) ).
cnf(33,axiom,
( ~ leaf(X,Y)
| ~ min_precedes(X,Z,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_21) ).
cnf(36,axiom,
( ~ next_subocc(X,Y,Z)
| min_precedes(X,Y,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_22) ).
cnf(37,axiom,
( ~ next_subocc(X,Y,Z)
| ~ min_precedes(X,U,Z)
| ~ min_precedes(U,Y,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_22) ).
cnf(44,axiom,
( ~ subactivity_occurrence(X,Y)
| activity_occurrence(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_24) ).
cnf(46,axiom,
( ~ min_precedes(X,Y,Z)
| occurrence_of('SKOLEMAAAV10'(Z,X,Y),Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_25) ).
cnf(47,axiom,
( ~ min_precedes(X,Y,Z)
| subactivity_occurrence(X,'SKOLEMAAAV10'(Z,X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_25) ).
cnf(48,axiom,
( ~ min_precedes(X,Y,Z)
| subactivity_occurrence(Y,'SKOLEMAAAV10'(Z,X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_25) ).
cnf(51,axiom,
( ~ occurrence_of(X,Y)
| atomic(Y)
| root('SKOLEMAAAV12'(Y,X),Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_27) ).
cnf(52,axiom,
( ~ occurrence_of(X,Y)
| atomic(Y)
| subactivity_occurrence('SKOLEMAAAV12'(Y,X),X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_27) ).
cnf(53,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(59,axiom,
( ~ root_occ(X,Y)
| occurrence_of(Y,'SKOLEMAAAV14'(Y,X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_33) ).
cnf(60,axiom,
( ~ root_occ(X,Y)
| subactivity_occurrence(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_33) ).
cnf(61,axiom,
( ~ root_occ(X,Y)
| root(X,'SKOLEMAAAV14'(Y,X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_33) ).
cnf(63,axiom,
( ~ leaf_occ(X,Y)
| occurrence_of(Y,'SKOLEMAAAV15'(Y,X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_34) ).
cnf(64,axiom,
( ~ leaf_occ(X,Y)
| subactivity_occurrence(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_34) ).
cnf(65,axiom,
( ~ leaf_occ(X,Y)
| leaf(X,'SKOLEMAAAV15'(Y,X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_34) ).
cnf(67,axiom,
( ~ occurrence_of(X,tptp0)
| occurrence_of('SKOLEMAAAV16'(X),tptp4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_35) ).
cnf(68,axiom,
( ~ occurrence_of(X,tptp0)
| root_occ('SKOLEMAAAV16'(X),X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_35) ).
cnf(69,axiom,
( ~ occurrence_of(X,tptp0)
| occurrence_of('SKOLEMAAAV17'(X),tptp3)
| occurrence_of('SKOLEMAAAV17'(X),tptp2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_35) ).
cnf(70,axiom,
( ~ occurrence_of(X,tptp0)
| leaf_occ('SKOLEMAAAV17'(X),X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_35) ).
cnf(71,axiom,
( ~ occurrence_of(X,tptp0)
| next_subocc('SKOLEMAAAV16'(X),'SKOLEMAAAV17'(X),tptp0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_35) ).
cnf(74,axiom,
atomic(tptp4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_38) ).
cnf(89,axiom,
( ~ send_message(X,Y,Z,U,V)
| X != tptp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_49) ).
cnf(90,axiom,
( ~ send_message(X,Y,Z,U,V)
| X != tptp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_49) ).
cnf(91,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_50) ).
cnf(93,axiom,
( ~ tptp1(X,Y,Z)
| ~ atomic(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_51) ).
cnf(95,axiom,
( ~ tptp1(X,Y,Z)
| root(Z,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_51) ).
cnf(96,axiom,
( ~ tptp1(X,Y,Z)
| ~ occurrence_of(U,X)
| send_message('SKOLEMAAAV18'(Z,Y,U),'SKOLEMAAAV19'(Z,Y,U),'SKOLEMAAAV20'(Z,Y,U),Z,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_52) ).
cnf(97,axiom,
( ~ tptp1(X,Y,Z)
| ~ occurrence_of(U,X)
| occurrence_of('SKOLEMAAAV21'(Z,Y,U),'SKOLEMAAAV18'(Z,Y,U)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_52) ).
cnf(98,axiom,
( ~ tptp1(X,Y,Z)
| ~ occurrence_of(U,X)
| root_occ('SKOLEMAAAV21'(Z,Y,U),U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_52) ).
cnf(100,negated_conjecture,
tptp1('SKOLEMAAAV22',tptp0,'SKOLEMAAAV23'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
cnf(101,negated_conjecture,
occurrence_of('SKOLEMAAAV24','SKOLEMAAAV22'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
cnf(109,plain,
~ atomic('SKOLEMAAAV22'),
inference('UR-RESOLVE',[status(thm)],[93,100]) ).
cnf(118,plain,
root('SKOLEMAAAV23',tptp0),
inference('HYPERRESOLVE',[status(thm)],[95,100]) ).
cnf(123,plain,
root('SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'),'SKOLEMAAAV22'),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[51,101]),109]) ).
cnf(124,plain,
subactivity_occurrence('SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'),'SKOLEMAAAV24'),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[52,101]),109]) ).
cnf(125,plain,
root_occ('SKOLEMAAAV21'('SKOLEMAAAV23',tptp0,'SKOLEMAAAV24'),'SKOLEMAAAV24'),
inference('HYPERRESOLVE',[status(thm)],[98,100,101]) ).
cnf(126,plain,
occurrence_of('SKOLEMAAAV21'('SKOLEMAAAV23',tptp0,'SKOLEMAAAV24'),'SKOLEMAAAV18'('SKOLEMAAAV23',tptp0,'SKOLEMAAAV24')),
inference('HYPERRESOLVE',[status(thm)],[97,100,101]) ).
cnf(127,plain,
send_message('SKOLEMAAAV18'('SKOLEMAAAV23',tptp0,'SKOLEMAAAV24'),'SKOLEMAAAV19'('SKOLEMAAAV23',tptp0,'SKOLEMAAAV24'),'SKOLEMAAAV20'('SKOLEMAAAV23',tptp0,'SKOLEMAAAV24'),'SKOLEMAAAV23',tptp0),
inference('HYPERRESOLVE',[status(thm)],[96,100,101]) ).
cnf(133,plain,
legal('SKOLEMAAAV23'),
inference('HYPERRESOLVE',[status(thm)],[27,118]) ).
cnf(134,plain,
~ min_precedes(X,'SKOLEMAAAV23',tptp0),
inference('UR-RESOLVE',[status(thm)],[25,118]) ).
cnf(145,plain,
arboreal('SKOLEMAAAV23'),
inference('HYPERRESOLVE',[status(thm)],[12,133]) ).
cnf(158,plain,
legal('SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24')),
inference('HYPERRESOLVE',[status(thm)],[27,123]) ).
cnf(159,plain,
~ min_precedes(X,'SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'),'SKOLEMAAAV22'),
inference('UR-RESOLVE',[status(thm)],[25,123]) ).
cnf(165,plain,
activity_occurrence('SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24')),
inference('HYPERRESOLVE',[status(thm)],[44,124]) ).
cnf(179,plain,
arboreal('SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24')),
inference('HYPERRESOLVE',[status(thm)],[12,158]) ).
cnf(182,plain,
occurrence_of('SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'),'SKOLEMAAAV1'('SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),
inference('HYPERRESOLVE',[status(thm)],[4,165]) ).
cnf(183,plain,
subactivity_occurrence('SKOLEMAAAV21'('SKOLEMAAAV23',tptp0,'SKOLEMAAAV24'),'SKOLEMAAAV24'),
inference('HYPERRESOLVE',[status(thm)],[60,125]) ).
cnf(184,plain,
occurrence_of('SKOLEMAAAV24','SKOLEMAAAV14'('SKOLEMAAAV24','SKOLEMAAAV21'('SKOLEMAAAV23',tptp0,'SKOLEMAAAV24'))),
inference('HYPERRESOLVE',[status(thm)],[59,125]) ).
cnf(185,plain,
root('SKOLEMAAAV21'('SKOLEMAAAV23',tptp0,'SKOLEMAAAV24'),'SKOLEMAAAV14'('SKOLEMAAAV24','SKOLEMAAAV21'('SKOLEMAAAV23',tptp0,'SKOLEMAAAV24'))),
inference('HYPERRESOLVE',[status(thm)],[61,125]) ).
cnf(318,plain,
'SKOLEMAAAV14'('SKOLEMAAAV24','SKOLEMAAAV21'('SKOLEMAAAV23',tptp0,'SKOLEMAAAV24')) = 'SKOLEMAAAV22',
inference('HYPERRESOLVE',[status(thm)],[5,184,101]) ).
cnf(319,plain,
root('SKOLEMAAAV21'('SKOLEMAAAV23',tptp0,'SKOLEMAAAV24'),'SKOLEMAAAV22'),
inference('REWRITE',[status(thm)],[185,318,theory(equality)]) ).
cnf(320,plain,
legal('SKOLEMAAAV21'('SKOLEMAAAV23',tptp0,'SKOLEMAAAV24')),
inference('HYPERRESOLVE',[status(thm)],[27,319]) ).
cnf(321,plain,
~ min_precedes(X,'SKOLEMAAAV21'('SKOLEMAAAV23',tptp0,'SKOLEMAAAV24'),'SKOLEMAAAV22'),
inference('UR-RESOLVE',[status(thm)],[25,319]) ).
cnf(327,plain,
arboreal('SKOLEMAAAV21'('SKOLEMAAAV23',tptp0,'SKOLEMAAAV24')),
inference('HYPERRESOLVE',[status(thm)],[12,320]) ).
cnf(333,plain,
'SKOLEMAAAV21'('SKOLEMAAAV23',tptp0,'SKOLEMAAAV24') = 'SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[53,327,101,179,183,124]),321,159]) ).
cnf(334,plain,
occurrence_of('SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'),'SKOLEMAAAV18'('SKOLEMAAAV23',tptp0,'SKOLEMAAAV24')),
inference('REWRITE',[status(thm)],[126,333,theory(equality)]) ).
cnf(389,plain,
'SKOLEMAAAV1'('SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24')) = 'SKOLEMAAAV18'('SKOLEMAAAV23',tptp0,'SKOLEMAAAV24'),
inference('HYPERRESOLVE',[status(thm)],[5,182,334]) ).
cnf(390,plain,
send_message('SKOLEMAAAV1'('SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24')),'SKOLEMAAAV19'('SKOLEMAAAV23',tptp0,'SKOLEMAAAV24'),'SKOLEMAAAV20'('SKOLEMAAAV23',tptp0,'SKOLEMAAAV24'),'SKOLEMAAAV23',tptp0),
inference('REWRITE',[status(thm)],[127,389,theory(equality)]) ).
cnf(666,plain,
'SKOLEMAAAV1'('SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24')) != tptp2,
inference('UR-RESOLVE',[status(thm)],[90,390]) ).
cnf(667,plain,
'SKOLEMAAAV1'('SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24')) != tptp3,
inference('UR-RESOLVE',[status(thm)],[89,390]) ).
cnf(669,plain,
min_precedes('SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'),tptp0),
inference('HYPERRESOLVE',[status(thm)],[91,390,182]) ).
cnf(672,plain,
~ occurrence_of('SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'),tptp2),
inference('UR-RESOLVE',[status(thm)],[5,666,182]) ).
cnf(673,plain,
~ occurrence_of('SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'),tptp3),
inference('UR-RESOLVE',[status(thm)],[5,667,182]) ).
cnf(715,plain,
subactivity_occurrence('SKOLEMAAAV23','SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),
inference('HYPERRESOLVE',[status(thm)],[47,669]) ).
cnf(716,plain,
occurrence_of('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24')),tptp0),
inference('HYPERRESOLVE',[status(thm)],[46,669]) ).
cnf(720,plain,
subactivity_occurrence('SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'),'SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),
inference('HYPERRESOLVE',[status(thm)],[48,669]) ).
cnf(866,plain,
occurrence_of('SKOLEMAAAV16'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),tptp4),
inference('HYPERRESOLVE',[status(thm)],[67,716]) ).
cnf(868,plain,
leaf_occ('SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),'SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),
inference('HYPERRESOLVE',[status(thm)],[70,716]) ).
cnf(869,plain,
root_occ('SKOLEMAAAV16'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),'SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),
inference('HYPERRESOLVE',[status(thm)],[68,716]) ).
cnf(871,plain,
next_subocc('SKOLEMAAAV16'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),'SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),tptp0),
inference('HYPERRESOLVE',[status(thm)],[71,716]) ).
cnf(872,plain,
( occurrence_of('SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),tptp3)
| occurrence_of('SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),tptp2) ),
inference('HYPERRESOLVE',[status(thm)],[69,716]) ).
cnf(1134,plain,
arboreal('SKOLEMAAAV16'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24')))),
inference('HYPERRESOLVE',[status(thm)],[11,866,74]) ).
cnf(2005,plain,
subactivity_occurrence('SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),'SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),
inference('HYPERRESOLVE',[status(thm)],[64,868]) ).
cnf(2006,plain,
occurrence_of('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24')),'SKOLEMAAAV15'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24')),'SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))))),
inference('HYPERRESOLVE',[status(thm)],[63,868]) ).
cnf(2007,plain,
leaf('SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),'SKOLEMAAAV15'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24')),'SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))))),
inference('HYPERRESOLVE',[status(thm)],[65,868]) ).
cnf(2008,plain,
subactivity_occurrence('SKOLEMAAAV16'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),'SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),
inference('HYPERRESOLVE',[status(thm)],[60,869]) ).
cnf(2009,plain,
occurrence_of('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24')),'SKOLEMAAAV14'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24')),'SKOLEMAAAV16'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))))),
inference('HYPERRESOLVE',[status(thm)],[59,869]) ).
cnf(2010,plain,
root('SKOLEMAAAV16'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),'SKOLEMAAAV14'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24')),'SKOLEMAAAV16'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))))),
inference('HYPERRESOLVE',[status(thm)],[61,869]) ).
cnf(2288,plain,
( min_precedes('SKOLEMAAAV23','SKOLEMAAAV16'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),tptp0)
| 'SKOLEMAAAV16'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))) = 'SKOLEMAAAV23' ),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[53,2008,716,1134,145,715]),134]) ).
cnf(2339,plain,
min_precedes('SKOLEMAAAV16'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),'SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),tptp0),
inference('HYPERRESOLVE',[status(thm)],[36,871]) ).
cnf(2856,plain,
precedes('SKOLEMAAAV16'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),'SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24')))),
inference('HYPERRESOLVE',[status(thm)],[26,2339]) ).
cnf(2957,plain,
legal('SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24')))),
inference('HYPERRESOLVE',[status(thm)],[15,2856]) ).
cnf(2959,plain,
arboreal('SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24')))),
inference('HYPERRESOLVE',[status(thm)],[12,2957]) ).
cnf(2972,plain,
( min_precedes('SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),'SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'),tptp0)
| min_precedes('SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'),'SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),tptp0)
| 'SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))) = 'SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24') ),
inference('HYPERRESOLVE',[status(thm)],[53,2959,716,179,2005,720]) ).
cnf(6147,plain,
'SKOLEMAAAV15'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24')),'SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24')))) = tptp0,
inference('HYPERRESOLVE',[status(thm)],[5,2006,716]) ).
cnf(6148,plain,
leaf('SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),tptp0),
inference('REWRITE',[status(thm)],[2007,6147,theory(equality)]) ).
cnf(6149,plain,
~ min_precedes('SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),X,tptp0),
inference('UR-RESOLVE',[status(thm)],[33,6148]) ).
cnf(6150,plain,
( min_precedes('SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'),'SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),tptp0)
| 'SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))) = 'SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24') ),
inference('REWRITE',[status(thm)],[2972,6149]) ).
cnf(6184,plain,
'SKOLEMAAAV14'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24')),'SKOLEMAAAV16'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24')))) = tptp0,
inference('HYPERRESOLVE',[status(thm)],[5,2009,716]) ).
cnf(6185,plain,
root('SKOLEMAAAV16'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),tptp0),
inference('REWRITE',[status(thm)],[2010,6184,theory(equality)]) ).
cnf(6186,plain,
~ min_precedes(X,'SKOLEMAAAV16'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),tptp0),
inference('UR-RESOLVE',[status(thm)],[25,6185]) ).
cnf(6188,plain,
'SKOLEMAAAV16'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))) = 'SKOLEMAAAV23',
inference('REWRITE',[status(thm)],[2288,6186]) ).
cnf(6189,plain,
next_subocc('SKOLEMAAAV23','SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),tptp0),
inference('REWRITE',[status(thm)],[871,6188,theory(equality)]) ).
cnf(6191,plain,
~ min_precedes('SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'),'SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))),tptp0),
inference('UR-RESOLVE',[status(thm)],[37,6189,669]) ).
cnf(6192,plain,
'SKOLEMAAAV17'('SKOLEMAAAV10'(tptp0,'SKOLEMAAAV23','SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'))) = 'SKOLEMAAAV12'('SKOLEMAAAV22','SKOLEMAAAV24'),
inference('REWRITE',[status(thm)],[6150,6191]) ).
cnf(6194,plain,
$false,
inference('REWRITE',[status(thm)],[872,672,673,6192,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : PRO002+1 : TPTP v8.1.0. Released v4.0.0.
% 0.12/0.13 % Command : run-snark %s %d
% 0.13/0.34 % Computer : n021.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 02:59:26 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.19/0.45 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.46 *
% 0.19/0.46 *
% 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-13T02:59:26
% 0.19/0.47 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n021.cluster.edu at 2022-06-13T02:59:26
% 4.11/4.31
% 4.11/4.31
% 4.11/4.31 #||
% 4.11/4.31 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.11/4.31 % SZS output start Refutation
% See solution above
% 4.11/4.32 ||#
% 4.11/4.32
% 4.11/4.32 ; Summary of computation:
% 4.11/4.32 ; 26156 formulas have been input or derived (from 2645 formulas).
% 4.11/4.32 ; 6194 (24%) were retained. Of these,
% 4.11/4.32 ; 3839 (62%) were simplified or subsumed later,
% 4.11/4.32 ; 2355 (38%) are still being kept.
% 4.11/4.32 ;
% 4.11/4.32 ; Run time in seconds excluding printing time:
% 4.11/4.32 ; 0.012 0% Read assertion file (1 call)
% 4.11/4.32 ; 0.003 0% Assert (55 calls)
% 4.11/4.32 ; 0.519 14% Process new row (22,771 calls)
% 4.11/4.32 ; 1.952 51% Resolution (5,288 calls)
% 4.11/4.32 ; 0.029 1% Paramodulation (2,644 calls)
% 4.11/4.32 ; 0.001 0% Factoring (354 calls)
% 4.11/4.32 ; 0.005 0% Condensing (2,916 calls)
% 4.11/4.32 ; 0.489 13% Forward subsumption (2,916 calls)
% 4.11/4.32 ; 0.090 2% Backward subsumption (1,765 calls)
% 4.11/4.32 ; 0.007 0% Clause clause subsumption (3,170 calls)
% 4.11/4.32 ; 0.247 6% Forward simplification (19,926 calls)
% 4.11/4.32 ; 0.362 9% Backward simplification (6,194 calls)
% 4.11/4.32 ; 0.009 0% Ordering (4,463 calls)
% 4.11/4.32 ; 0.000 0% Sortal reasoning (32 calls)
% 4.11/4.32 ; 0.001 0% Purity testing (1 call)
% 4.11/4.32 ; 0.115 3% Other
% 4.11/4.32 ; 3.841 Total
% 4.11/4.32 ; 3.851 Real time
% 4.11/4.32 ;
% 4.11/4.32 ; Term-hash-array has 7,635 terms in all.
% 4.11/4.32 ; Feature-vector-row-index has 1,016 entries (1,200 at peak, 1,765 added, 749 deleted).
% 4.11/4.32 ; Feature-vector-row-index has 12,169 nodes (16,020 at peak, 24,562 added, 12,393 deleted).
% 4.11/4.32 ; Retrieved 5,844 possibly forward subsuming rows in 2,916 calls.
% 4.11/4.32 ; Retrieved 254 possibly backward subsumed rows in 1,765 calls.
% 4.11/4.32 ; Path-index has 2,965 entries (4,262 at peak, 7,753 added, 4,788 deleted).
% 4.11/4.32 ; Path-index has 23,882 nodes (25,128 at peak, 31,053 added, 7,171 deleted).
% 4.11/4.32 ; Trie-index has 2,965 entries (4,262 at peak, 7,753 added, 4,788 deleted).
% 4.11/4.32 ; Trie-index has 23,187 nodes (31,451 at peak, 58,581 added, 35,394 deleted).
% 4.11/4.32 ; Retrieved 13,120 generalization terms in 55,481 calls.
% 4.11/4.32 ; Retrieved 4,543 instance terms in 4,428 calls.
% 4.11/4.32 ; Retrieved 1,510,983 unifiable terms in 288,512 calls.
% 4.11/4.32 ;
% 4.11/4.32 ; The agenda of backward simplifiable rows to process has 399 entries:
% 4.11/4.32 ; 399 with value 0
% 4.11/4.32 ; The agenda of rows to process has 4 entries:
% 4.11/4.32 ; 1 with value 23 1 with value 27 1 with value 29
% 4.11/4.32 ; 1 with value 24
% 4.11/4.32 ; The agenda of rows to give has 974 entries:
% 4.11/4.32 ; 1 with value (4 19) 11 with value (4 51) 3 with value (4 71)
% 4.11/4.32 ; 1 with value (4 21) 9 with value (4 52) 5 with value (4 72)
% 4.11/4.32 ; 1 with value (4 26) 12 with value (4 53) 4 with value (4 73)
% 4.11/4.32 ; 93 with value (4 33) 14 with value (4 54) 2 with value (4 74)
% 4.11/4.32 ; 91 with value (4 34) 15 with value (4 55) 2 with value (4 75)
% 4.11/4.32 ; 81 with value (4 35) 9 with value (4 56) 4 with value (4 76)
% 4.11/4.32 ; 61 with value (4 36) 7 with value (4 57) 1 with value (4 77)
% 4.11/4.32 ; 47 with value (4 37) 11 with value (4 58) 4 with value (4 78)
% 4.11/4.32 ; 67 with value (4 38) 9 with value (4 59) 1 with value (4 79)
% 4.11/4.32 ; 52 with value (4 39) 4 with value (4 60) 2 with value (4 80)
% 4.11/4.32 ; 39 with value (4 40) 6 with value (4 61) 3 with value (4 81)
% 4.11/4.32 ; 28 with value (4 41) 4 with value (4 62) 2 with value (4 83)
% 4.11/4.32 ; 32 with value (4 42) 6 with value (4 63) 2 with value (4 84)
% 4.11/4.32 ; 26 with value (4 43) 11 with value (4 64) 1 with value (4 85)
% 4.11/4.32 ; 25 with value (4 44) 8 with value (4 65) 2 with value (4 86)
% 4.11/4.32 ; 33 with value (4 45) 4 with value (4 66) 2 with value (4 88)
% 4.11/4.32 ; 18 with value (4 46) 2 with value (4 67) 3 with value (4 89)
% 4.11/4.32 ; 20 with value (4 47) 9 with value (4 68) 2 with value (4 91)
% 4.11/4.32 ; 13 with value (4 48) 3 with value (4 69) 1 with value (4 95)
% 4.11/4.32 ; 17 with value (4 49) 8 with value (4 70) 1 with value (4 96)
% 4.11/4.32 ; 19 with value (4 50)
% 4.11/4.32 Evaluation took:
% 4.11/4.32 3.853 seconds of real time
% 4.11/4.32 3.634172 seconds of user run time
% 4.11/4.32 0.217997 seconds of system run time
% 4.11/4.32 [Run times include 0.566 seconds GC run time.]
% 4.11/4.32 0 calls to %EVAL
% 4.11/4.32 0 page faults and
% 4.11/4.32 376,929,008 bytes consed.
% 4.11/4.32 :PROOF-FOUND
% 4.11/4.32 ; End refute-file /export/starexec/sandbox/benchmark/theBenchmark.p 2022-06-13T02:59:30
% 4.11/4.32 :PROOF-FOUND
% 4.11/4.32 *
%------------------------------------------------------------------------------