%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : KRS144+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% Computer : n024.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 : Sun Jul 17 03:28:52 EDT 2022
% Result : Theorem 38.66s 38.85s
% Output : Refutation 38.66s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
cnf(8,axiom,
cowlThing(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_0) ).
cnf(9,axiom,
~ cowlNothing(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_0) ).
cnf(10,axiom,
( ~ xsd_string(X)
| ~ xsd_integer(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1) ).
cnf(11,axiom,
( xsd_string(X)
| xsd_integer(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1) ).
cnf(12,axiom,
( ~ cc(X)
| rp(X,'SKOLEMAAAV1'(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
cnf(13,axiom,
( ~ cc(X)
| rp(X,'SKOLEMAAAV2'(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
cnf(14,axiom,
( ~ cc(X)
| 'SKOLEMAAAV1'(X) != 'SKOLEMAAAV2'(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
cnf(15,axiom,
( ~ cc(X)
| ~ rp(X,Y)
| ~ rp(X,Z)
| ~ rp(X,U)
| Y = Z
| Y = U
| Z = U ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
cnf(16,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| cc('SKOLEMAAAV5')
| cc('SKOLEMAAAV9') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(17,plain,
( ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| cc('SKOLEMAAAV5')
| cc('SKOLEMAAAV9') ),
inference('REWRITE',[status(thm)],[16,9,8]) ).
cnf(18,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| cc('SKOLEMAAAV5')
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(19,plain,
( ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| cc('SKOLEMAAAV5')
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
inference('REWRITE',[status(thm)],[18,9,8]) ).
cnf(20,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV6')
| cc('SKOLEMAAAV9') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(21,plain,
( ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV6')
| cc('SKOLEMAAAV9') ),
inference('REWRITE',[status(thm)],[20,9,8]) ).
cnf(22,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV6')
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(23,plain,
( ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV6')
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
inference('REWRITE',[status(thm)],[22,9,8]) ).
cnf(24,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV7')
| cc('SKOLEMAAAV9') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(25,plain,
( ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV7')
| cc('SKOLEMAAAV9') ),
inference('REWRITE',[status(thm)],[24,9,8]) ).
cnf(26,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV7')
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(27,plain,
( ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV7')
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
inference('REWRITE',[status(thm)],[26,9,8]) ).
cnf(28,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV8')
| cc('SKOLEMAAAV9') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(29,plain,
( ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV8')
| cc('SKOLEMAAAV9') ),
inference('REWRITE',[status(thm)],[28,9,8]) ).
cnf(30,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV8')
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(31,plain,
( ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV8')
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
inference('REWRITE',[status(thm)],[30,9,8]) ).
cnf(32,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV6' != 'SKOLEMAAAV7'
| cc('SKOLEMAAAV9') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(33,plain,
( ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV6' != 'SKOLEMAAAV7'
| cc('SKOLEMAAAV9') ),
inference('REWRITE',[status(thm)],[32,9,8]) ).
cnf(34,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV6' != 'SKOLEMAAAV7'
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(35,plain,
( ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV6' != 'SKOLEMAAAV7'
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
inference('REWRITE',[status(thm)],[34,9,8]) ).
cnf(36,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV6' != 'SKOLEMAAAV8'
| cc('SKOLEMAAAV9') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(37,plain,
( ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV6' != 'SKOLEMAAAV8'
| cc('SKOLEMAAAV9') ),
inference('REWRITE',[status(thm)],[36,9,8]) ).
cnf(38,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV6' != 'SKOLEMAAAV8'
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(39,plain,
( ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV6' != 'SKOLEMAAAV8'
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
inference('REWRITE',[status(thm)],[38,9,8]) ).
cnf(40,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV7' != 'SKOLEMAAAV8'
| cc('SKOLEMAAAV9') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(41,plain,
( ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV7' != 'SKOLEMAAAV8'
| cc('SKOLEMAAAV9') ),
inference('REWRITE',[status(thm)],[40,9,8]) ).
cnf(42,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV7' != 'SKOLEMAAAV8'
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(43,plain,
( ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV7' != 'SKOLEMAAAV8'
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
inference('REWRITE',[status(thm)],[42,9,8]) ).
cnf(44,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| cc('SKOLEMAAAV5')
| cc('SKOLEMAAAV9') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(45,plain,
( xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| cc('SKOLEMAAAV5')
| cc('SKOLEMAAAV9') ),
inference('REWRITE',[status(thm)],[44,9,8]) ).
cnf(46,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| cc('SKOLEMAAAV5')
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(47,plain,
( xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| cc('SKOLEMAAAV5')
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
inference('REWRITE',[status(thm)],[46,9,8]) ).
cnf(48,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV6')
| cc('SKOLEMAAAV9') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(49,plain,
( xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV6')
| cc('SKOLEMAAAV9') ),
inference('REWRITE',[status(thm)],[48,9,8]) ).
cnf(50,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV6')
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(51,plain,
( xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV6')
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
inference('REWRITE',[status(thm)],[50,9,8]) ).
cnf(52,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV7')
| cc('SKOLEMAAAV9') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(53,plain,
( xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV7')
| cc('SKOLEMAAAV9') ),
inference('REWRITE',[status(thm)],[52,9,8]) ).
cnf(54,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV7')
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(55,plain,
( xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV7')
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
inference('REWRITE',[status(thm)],[54,9,8]) ).
cnf(56,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV8')
| cc('SKOLEMAAAV9') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(57,plain,
( xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV8')
| cc('SKOLEMAAAV9') ),
inference('REWRITE',[status(thm)],[56,9,8]) ).
cnf(58,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV8')
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(59,plain,
( xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV8')
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
inference('REWRITE',[status(thm)],[58,9,8]) ).
cnf(60,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV6' != 'SKOLEMAAAV7'
| cc('SKOLEMAAAV9') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(61,plain,
( xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV6' != 'SKOLEMAAAV7'
| cc('SKOLEMAAAV9') ),
inference('REWRITE',[status(thm)],[60,9,8]) ).
cnf(62,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV6' != 'SKOLEMAAAV7'
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(63,plain,
( xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV6' != 'SKOLEMAAAV7'
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
inference('REWRITE',[status(thm)],[62,9,8]) ).
cnf(64,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV6' != 'SKOLEMAAAV8'
| cc('SKOLEMAAAV9') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(65,plain,
( xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV6' != 'SKOLEMAAAV8'
| cc('SKOLEMAAAV9') ),
inference('REWRITE',[status(thm)],[64,9,8]) ).
cnf(66,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV6' != 'SKOLEMAAAV8'
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(67,plain,
( xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV6' != 'SKOLEMAAAV8'
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
inference('REWRITE',[status(thm)],[66,9,8]) ).
cnf(68,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV7' != 'SKOLEMAAAV8'
| cc('SKOLEMAAAV9') ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(69,plain,
( xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV7' != 'SKOLEMAAAV8'
| cc('SKOLEMAAAV9') ),
inference('REWRITE',[status(thm)],[68,9,8]) ).
cnf(70,negated_conjecture,
( ~ cowlThing('SKOLEMAAAV3')
| cowlNothing('SKOLEMAAAV3')
| xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV7' != 'SKOLEMAAAV8'
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
cnf(71,plain,
( xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV7' != 'SKOLEMAAAV8'
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
inference('REWRITE',[status(thm)],[70,9,8]) ).
cnf(72,plain,
( xsd_integer('SKOLEMAAAV4')
| cc('SKOLEMAAAV5')
| cc('SKOLEMAAAV9') ),
inference('HYPERRESOLVE',[status(thm)],[17,11]) ).
cnf(73,plain,
( xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV6')
| cc('SKOLEMAAAV9') ),
inference('HYPERRESOLVE',[status(thm)],[21,11]) ).
cnf(74,plain,
( xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV7')
| cc('SKOLEMAAAV9') ),
inference('HYPERRESOLVE',[status(thm)],[25,11]) ).
cnf(75,plain,
( xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV8')
| cc('SKOLEMAAAV9') ),
inference('HYPERRESOLVE',[status(thm)],[29,11]) ).
cnf(76,plain,
( cc('SKOLEMAAAV5')
| cc('SKOLEMAAAV9')
| xsd_string('SKOLEMAAAV4') ),
inference('HYPERRESOLVE',[status(thm)],[45,72]) ).
cnf(77,plain,
( cc('SKOLEMAAAV5')
| cc('SKOLEMAAAV9') ),
inference('HYPERRESOLVE',[status(thm)],[10,76,72]) ).
cnf(78,plain,
( cc('SKOLEMAAAV5')
| rp('SKOLEMAAAV9','SKOLEMAAAV2'('SKOLEMAAAV9')) ),
inference('HYPERRESOLVE',[status(thm)],[13,77]) ).
cnf(79,plain,
( cc('SKOLEMAAAV5')
| rp('SKOLEMAAAV9','SKOLEMAAAV1'('SKOLEMAAAV9')) ),
inference('HYPERRESOLVE',[status(thm)],[12,77]) ).
cnf(80,plain,
( cc('SKOLEMAAAV5')
| xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9') ),
inference('HYPERRESOLVE',[status(thm)],[19,79,11,78]) ).
cnf(81,plain,
( cc('SKOLEMAAAV5')
| 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9')
| xsd_string('SKOLEMAAAV4') ),
inference('HYPERRESOLVE',[status(thm)],[47,80,78,79]) ).
cnf(82,plain,
( cc('SKOLEMAAAV5')
| 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9') ),
inference('HYPERRESOLVE',[status(thm)],[10,81,80]) ).
cnf(85,plain,
( 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9')
| xsd_integer('SKOLEMAAAV4')
| cc('SKOLEMAAAV9')
| 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8' ),
inference('HYPERRESOLVE',[status(thm)],[15,82,73,74,75]) ).
cnf(95,plain,
( 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9')
| cc('SKOLEMAAAV9')
| 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8'
| xsd_string('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV8') ),
inference('HYPERRESOLVE',[status(thm)],[57,85]) ).
cnf(96,plain,
( 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9')
| cc('SKOLEMAAAV9')
| 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8'
| xsd_string('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV7') ),
inference('HYPERRESOLVE',[status(thm)],[53,85]) ).
cnf(97,plain,
( 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9')
| cc('SKOLEMAAAV9')
| 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8'
| xsd_string('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV6') ),
inference('HYPERRESOLVE',[status(thm)],[49,85]) ).
cnf(120,plain,
( 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9')
| cc('SKOLEMAAAV9')
| 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8'
| xsd_string('SKOLEMAAAV4') ),
inference('HYPERRESOLVE',[status(thm)],[15,97,82,96,95]) ).
cnf(121,plain,
( 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9')
| cc('SKOLEMAAAV9')
| 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8' ),
inference('HYPERRESOLVE',[status(thm)],[10,120,85]) ).
cnf(122,plain,
( 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9')
| 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8'
| rp('SKOLEMAAAV9','SKOLEMAAAV2'('SKOLEMAAAV9')) ),
inference('HYPERRESOLVE',[status(thm)],[13,121]) ).
cnf(123,plain,
( 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9')
| 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8'
| rp('SKOLEMAAAV9','SKOLEMAAAV1'('SKOLEMAAAV9')) ),
inference('HYPERRESOLVE',[status(thm)],[12,121]) ).
cnf(124,plain,
( 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9')
| 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8'
| xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV8') ),
inference('HYPERRESOLVE',[status(thm)],[31,123,11,122]) ).
cnf(125,plain,
( 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9')
| 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8'
| xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV7') ),
inference('HYPERRESOLVE',[status(thm)],[27,123,11,122]) ).
cnf(126,plain,
( 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9')
| 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8'
| xsd_integer('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV6') ),
inference('HYPERRESOLVE',[status(thm)],[23,123,11,122]) ).
cnf(131,plain,
( 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9')
| 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8'
| xsd_integer('SKOLEMAAAV4') ),
inference('HYPERRESOLVE',[status(thm)],[15,126,82,125,124]) ).
cnf(132,plain,
( 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9')
| 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8'
| xsd_string('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV8') ),
inference('HYPERRESOLVE',[status(thm)],[59,131,122,123]) ).
cnf(133,plain,
( 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9')
| 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8'
| xsd_string('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV7') ),
inference('HYPERRESOLVE',[status(thm)],[55,131,122,123]) ).
cnf(134,plain,
( 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9')
| 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8'
| xsd_string('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV6') ),
inference('HYPERRESOLVE',[status(thm)],[51,131,122,123]) ).
cnf(148,plain,
( 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9')
| 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8'
| xsd_string('SKOLEMAAAV4') ),
inference('HYPERRESOLVE',[status(thm)],[15,134,82,133,132]) ).
cnf(149,plain,
( 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9')
| 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8' ),
inference('HYPERRESOLVE',[status(thm)],[10,148,131]) ).
cnf(150,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8'
| cc('SKOLEMAAAV5') ),
inference('HYPERRESOLVE',[status(thm)],[14,149,77]) ).
cnf(153,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8'
| ~ cc('SKOLEMAAAV9') ),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[14,149,theory(equality)]),theory(equality)]) ).
cnf(154,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8'
| xsd_integer('SKOLEMAAAV4')
| cc('SKOLEMAAAV9') ),
inference('HYPERRESOLVE',[status(thm)],[15,150,73,74,75]) ).
cnf(157,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8'
| cc('SKOLEMAAAV9')
| xsd_string('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV8') ),
inference('HYPERRESOLVE',[status(thm)],[57,154]) ).
cnf(158,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8'
| cc('SKOLEMAAAV9')
| xsd_string('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV7') ),
inference('HYPERRESOLVE',[status(thm)],[53,154]) ).
cnf(159,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8'
| cc('SKOLEMAAAV9')
| xsd_string('SKOLEMAAAV4')
| rp('SKOLEMAAAV5','SKOLEMAAAV6') ),
inference('HYPERRESOLVE',[status(thm)],[49,154]) ).
cnf(164,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8'
| cc('SKOLEMAAAV9')
| xsd_string('SKOLEMAAAV4') ),
inference('HYPERRESOLVE',[status(thm)],[15,159,150,158,157]) ).
cnf(165,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8'
| cc('SKOLEMAAAV9') ),
inference('HYPERRESOLVE',[status(thm)],[10,164,154]) ).
cnf(166,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV7' = 'SKOLEMAAAV8' ),
inference('HYPERRESOLVE',[status(thm)],[153,165]) ).
cnf(167,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| xsd_integer('SKOLEMAAAV4')
| cc('SKOLEMAAAV9') ),
inference('HYPERRESOLVE',[status(thm)],[41,166,11]) ).
cnf(180,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| cc('SKOLEMAAAV9')
| xsd_string('SKOLEMAAAV4') ),
inference('HYPERRESOLVE',[status(thm)],[69,167,166]) ).
cnf(181,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| cc('SKOLEMAAAV9') ),
inference('HYPERRESOLVE',[status(thm)],[10,180,167]) ).
cnf(182,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| rp('SKOLEMAAAV9','SKOLEMAAAV2'('SKOLEMAAAV9')) ),
inference('HYPERRESOLVE',[status(thm)],[13,181]) ).
cnf(183,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| rp('SKOLEMAAAV9','SKOLEMAAAV1'('SKOLEMAAAV9')) ),
inference('HYPERRESOLVE',[status(thm)],[12,181]) ).
cnf(184,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9') ),
inference('HYPERRESOLVE',[status(thm)],[43,183,11,166,182]) ).
cnf(311,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9')
| xsd_string('SKOLEMAAAV4') ),
inference('HYPERRESOLVE',[status(thm)],[71,184,166,182,183]) ).
cnf(419,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8'
| 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9') ),
inference('HYPERRESOLVE',[status(thm)],[10,311,184]) ).
cnf(420,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV6' = 'SKOLEMAAAV8' ),
inference('HYPERRESOLVE',[status(thm)],[14,419,181]) ).
cnf(421,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| xsd_integer('SKOLEMAAAV4')
| cc('SKOLEMAAAV9') ),
inference('HYPERRESOLVE',[status(thm)],[37,420,11]) ).
cnf(432,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| cc('SKOLEMAAAV9')
| xsd_string('SKOLEMAAAV4') ),
inference('HYPERRESOLVE',[status(thm)],[65,421,420]) ).
cnf(433,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| cc('SKOLEMAAAV9') ),
inference('HYPERRESOLVE',[status(thm)],[10,432,421]) ).
cnf(434,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| rp('SKOLEMAAAV9','SKOLEMAAAV2'('SKOLEMAAAV9')) ),
inference('HYPERRESOLVE',[status(thm)],[13,433]) ).
cnf(435,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| rp('SKOLEMAAAV9','SKOLEMAAAV1'('SKOLEMAAAV9')) ),
inference('HYPERRESOLVE',[status(thm)],[12,433]) ).
cnf(440,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| xsd_integer('SKOLEMAAAV4')
| 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9') ),
inference('HYPERRESOLVE',[status(thm)],[39,435,11,420,434]) ).
cnf(561,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9')
| xsd_string('SKOLEMAAAV4') ),
inference('HYPERRESOLVE',[status(thm)],[67,440,420,434,435]) ).
cnf(687,plain,
( 'SKOLEMAAAV6' = 'SKOLEMAAAV7'
| 'SKOLEMAAAV1'('SKOLEMAAAV9') = 'SKOLEMAAAV2'('SKOLEMAAAV9') ),
inference('HYPERRESOLVE',[status(thm)],[10,561,440]) ).
cnf(688,plain,
'SKOLEMAAAV6' = 'SKOLEMAAAV7',
inference('HYPERRESOLVE',[status(thm)],[14,687,433]) ).
cnf(689,plain,
( ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| cc('SKOLEMAAAV9') ),
inference('REWRITE',[status(thm)],[33,688,theory(equality)]) ).
cnf(690,plain,
( ~ xsd_string('SKOLEMAAAV4')
| xsd_integer('SKOLEMAAAV4')
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
inference('REWRITE',[status(thm)],[35,688,theory(equality)]) ).
cnf(691,plain,
( xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| cc('SKOLEMAAAV9') ),
inference('REWRITE',[status(thm)],[61,688,theory(equality)]) ).
cnf(692,plain,
( xsd_string('SKOLEMAAAV4')
| ~ xsd_integer('SKOLEMAAAV4')
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
inference('REWRITE',[status(thm)],[63,688,theory(equality)]) ).
cnf(693,plain,
( xsd_integer('SKOLEMAAAV4')
| cc('SKOLEMAAAV9') ),
inference('HYPERRESOLVE',[status(thm)],[689,11]) ).
cnf(694,plain,
( cc('SKOLEMAAAV9')
| xsd_string('SKOLEMAAAV4') ),
inference('HYPERRESOLVE',[status(thm)],[691,693]) ).
cnf(695,plain,
cc('SKOLEMAAAV9'),
inference('HYPERRESOLVE',[status(thm)],[10,694,693]) ).
cnf(696,plain,
rp('SKOLEMAAAV9','SKOLEMAAAV2'('SKOLEMAAAV9')),
inference('HYPERRESOLVE',[status(thm)],[13,695]) ).
cnf(697,plain,
rp('SKOLEMAAAV9','SKOLEMAAAV1'('SKOLEMAAAV9')),
inference('HYPERRESOLVE',[status(thm)],[12,695]) ).
cnf(698,plain,
'SKOLEMAAAV1'('SKOLEMAAAV9') != 'SKOLEMAAAV2'('SKOLEMAAAV9'),
inference('UR-RESOLVE',[status(thm)],[14,695]) ).
cnf(708,plain,
xsd_integer('SKOLEMAAAV4'),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[690,697,11,696]),698]) ).
cnf(709,plain,
( xsd_string('SKOLEMAAAV4')
| ~ rp('SKOLEMAAAV9',X)
| ~ rp('SKOLEMAAAV9',Y)
| X = Y ),
inference('REWRITE',[status(thm)],[692,708]) ).
cnf(710,plain,
xsd_string('SKOLEMAAAV4'),
inference('REWRITE',[status(thm)],[inference('HYPERRESOLVE',[status(thm)],[709,696,697]),698]) ).
cnf(711,plain,
$false,
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[10,708]),710]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : KRS144+1 : TPTP v8.1.0. Released v3.1.0.
% 0.03/0.12 % Command : run-snark %s %d
% 0.11/0.32 % Computer : n024.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 600
% 0.11/0.32 % DateTime : Tue Jun 7 10:55:50 EDT 2022
% 0.11/0.32 % CPUTime :
% 0.17/0.43 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 *
% 0.17/0.44 *
% 0.17/0.45 #<PACKAGE "SNARK-USER">
% 0.17/0.45 *
% 0.17/0.45 SNARK-TPTP-OPTIONS
% 0.17/0.45 *
% 0.17/0.45 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.17/0.45 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.17/0.45 (USE-FACTORING :POS)
% 0.17/0.45 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.17/0.45 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.17/0.45 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.17/0.45 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.17/0.45 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.17/0.45 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.17/0.45 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.17/0.45 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.17/0.45 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.17/0.45 (DECLARE-TPTP-SYMBOLS2))
% 0.17/0.45 *
% 0.17/0.45 "."
% 0.17/0.45 *
% 0.17/0.45 ; Begin refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-07T10:55:50
% 0.17/0.45 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n024.cluster.edu at 2022-06-07T10:55:50
% 38.66/38.85
% 38.66/38.85
% 38.66/38.85 #||
% 38.66/38.85 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 38.66/38.85 % SZS output start Refutation
% See solution above
% 38.66/38.86 ||#
% 38.66/38.86
% 38.66/38.86 ; Summary of computation:
% 38.66/38.86 ; 440632 formulas have been input or derived (from 427 formulas).
% 38.66/38.86 ; 711 ( 0%) were retained. Of these,
% 38.66/38.86 ; 667 (94%) were simplified or subsumed later,
% 38.66/38.86 ; 44 ( 6%) are still being kept.
% 38.66/38.86 ;
% 38.66/38.86 ; Run time in seconds excluding printing time:
% 38.66/38.86 ; 0.004 0% Read assertion file (1 call)
% 38.66/38.86 ; 0.001 0% Assert (11 calls)
% 38.66/38.86 ; 0.711 2% Process new row (280,363 calls)
% 38.66/38.86 ; 18.315 48% Resolution (852 calls)
% 38.66/38.86 ; 0.023 0% Paramodulation (426 calls)
% 38.66/38.86 ; 0.004 0% Factoring (354 calls)
% 38.66/38.86 ; 0.103 0% Condensing (52,511 calls)
% 38.66/38.86 ; 8.656 23% Forward subsumption (52,511 calls)
% 38.66/38.86 ; 0.050 0% Backward subsumption (670 calls)
% 38.66/38.86 ; 0.905 2% Clause clause subsumption (139,916 calls)
% 38.66/38.86 ; 8.783 23% Forward simplification (203,595 calls)
% 38.66/38.86 ; 0.003 0% Backward simplification (683 calls)
% 38.66/38.86 ; 0.024 0% Ordering (18,940 calls)
% 38.66/38.86 ; 0.000 0% Sortal reasoning (32 calls)
% 38.66/38.86 ; 0.001 0% Purity testing (1 call)
% 38.66/38.86 ; 0.814 2% Other
% 38.66/38.86 ; 38.397 Total
% 38.66/38.86 ; 38.414 Real time
% 38.66/38.86 ;
% 38.66/38.86 ; Term-hash-array has 67 terms in all.
% 38.66/38.86 ; Feature-vector-row-index has 31 entries (165 at peak, 670 added, 639 deleted).
% 38.66/38.86 ; Feature-vector-row-index has 108 nodes (929 at peak, 5,154 added, 5,046 deleted).
% 38.66/38.86 ; Retrieved 871,034 possibly forward subsuming rows in 52,511 calls.
% 38.66/38.86 ; Retrieved 1,042 possibly backward subsumed rows in 670 calls.
% 38.66/38.86 ; Path-index has 59 entries (72 at peak, 99 added, 40 deleted).
% 38.66/38.86 ; Path-index has 72 nodes (79 at peak, 103 added, 31 deleted).
% 38.66/38.86 ; Trie-index has 59 entries (72 at peak, 99 added, 40 deleted).
% 38.66/38.86 ; Trie-index has 83 nodes (97 at peak, 131 added, 48 deleted).
% 38.66/38.86 ; Retrieved 72 generalization terms in 95 calls.
% 38.66/38.86 ; Retrieved 14 instance terms in 12 calls.
% 38.66/38.86 ; Retrieved 259,241 unifiable terms in 37,382 calls.
% 38.66/38.86 ;
% 38.66/38.86 ; The agenda of rows to process has 1 entry:
% 38.66/38.86 ; 1 with value 9
% 38.66/38.86 ; The agenda of rows to give has 12 entries:
% 38.66/38.86 ; 1 with value (4 8) 2 with value (4 14) 2 with value (4 42)
% 38.66/38.86 ; 1 with value (4 10) 2 with value (4 39) 1 with value (4 43)
% 38.66/38.86 ; 1 with value (4 11) 2 with value (4 40)
% 38.66/38.86 Evaluation took:
% 38.66/38.86 38.414 seconds of real time
% 38.66/38.86 37.197815 seconds of user run time
% 38.66/38.86 1.212703 seconds of system run time
% 38.66/38.86 [Run times include 0.953 seconds GC run time.]
% 38.66/38.86 0 calls to %EVAL
% 38.66/38.86 0 page faults and
% 38.66/38.86 3,101,188,696 bytes consed.
% 38.66/38.86 :PROOF-FOUND
% 38.66/38.86 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-07T10:56:28
% 38.66/38.86 :PROOF-FOUND
% 38.66/38.86 *
%------------------------------------------------------------------------------