%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PUZ016-2.005 : TPTP v8.1.2. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %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 : 300s
% DateTime : Thu May 9 17:37:36 EDT 2024
% Result : Unsatisfiable 6.49s 6.66s
% Output : Refutation 6.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 68
% Number of leaves : 59
% Syntax : Number of clauses : 253 ( 17 unt; 154 nHn; 253 RR)
% Number of literals : 637 ( 0 equ; 180 neg)
% Maximal clause size : 4 ( 2 avg)
% Maximal term depth : 0 ( 0 avg)
% Number of predicates : 38 ( 37 usr; 38 prp; 0-0 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(unique_cover6_3_4,negated_conjecture,
( ~ horizontal_3_3
| ~ vertical_2_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover6_3_4) ).
cnf(unique_cover4_1_5,negated_conjecture,
( ~ vertical_1_5
| ~ horizontal_1_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover4_1_5) ).
cnf(covered_1_5,negated_conjecture,
( vertical_1_5
| horizontal_1_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',covered_1_5) ).
cnf(unique_cover5_2_5,negated_conjecture,
( ~ vertical_2_5
| ~ vertical_1_5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover5_2_5) ).
cnf(c31,plain,
( ~ vertical_2_5
| horizontal_1_4 ),
inference(resolution,[status(thm)],[unique_cover5_2_5,covered_1_5]) ).
cnf(covered_3_5,negated_conjecture,
( vertical_3_5
| horizontal_3_4
| vertical_2_5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',covered_3_5) ).
cnf(unique_cover5_4_5,negated_conjecture,
( ~ vertical_4_5
| ~ vertical_3_5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover5_4_5) ).
cnf(c123,plain,
( ~ vertical_4_5
| horizontal_3_4
| vertical_2_5 ),
inference(resolution,[status(thm)],[unique_cover5_4_5,covered_3_5]) ).
cnf(unique_cover6_4_5,negated_conjecture,
( ~ horizontal_4_4
| ~ vertical_3_5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover6_4_5) ).
cnf(unique_cover2_3_4,negated_conjecture,
( ~ horizontal_3_4
| ~ horizontal_3_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover2_3_4) ).
cnf(unique_cover3_5_3,negated_conjecture,
( ~ horizontal_5_3
| ~ vertical_4_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover3_5_3) ).
cnf(unique_cover3_5_1,negated_conjecture,
( ~ horizontal_5_1
| ~ vertical_4_1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover3_5_1) ).
cnf(covered_5_1,negated_conjecture,
( horizontal_5_1
| vertical_4_1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',covered_5_1) ).
cnf(unique_cover2_5_2,negated_conjecture,
( ~ horizontal_5_2
| ~ horizontal_5_1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover2_5_2) ).
cnf(c130,plain,
( ~ horizontal_5_2
| vertical_4_1 ),
inference(resolution,[status(thm)],[unique_cover2_5_2,covered_5_1]) ).
cnf(covered_5_5,negated_conjecture,
( horizontal_5_4
| vertical_4_5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',covered_5_5) ).
cnf(covered_5_3,negated_conjecture,
( horizontal_5_3
| horizontal_5_2
| vertical_4_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',covered_5_3) ).
cnf(unique_cover2_5_4,negated_conjecture,
( ~ horizontal_5_4
| ~ horizontal_5_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover2_5_4) ).
cnf(c143,plain,
( ~ horizontal_5_4
| horizontal_5_2
| vertical_4_3 ),
inference(resolution,[status(thm)],[unique_cover2_5_4,covered_5_3]) ).
cnf(c286,plain,
( horizontal_5_2
| vertical_4_3
| vertical_4_5 ),
inference(resolution,[status(thm)],[c143,covered_5_5]) ).
cnf(c374,plain,
( vertical_4_3
| vertical_4_5
| vertical_4_1 ),
inference(resolution,[status(thm)],[c286,c130]) ).
cnf(c480,plain,
( vertical_4_3
| vertical_4_5
| ~ horizontal_5_1 ),
inference(resolution,[status(thm)],[c374,unique_cover3_5_1]) ).
cnf(unique_cover3_5_2,negated_conjecture,
( ~ horizontal_5_2
| ~ vertical_4_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover3_5_2) ).
cnf(unique_cover4_3_2,negated_conjecture,
( ~ vertical_3_2
| ~ horizontal_3_1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover4_3_2) ).
cnf(unique_cover5_4_1,negated_conjecture,
( ~ vertical_4_1
| ~ vertical_3_1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover5_4_1) ).
cnf(uncovered3_1_2,negated_conjecture,
~ horizontal_1_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',uncovered3_1_2) ).
cnf(covered_1_1,negated_conjecture,
( horizontal_1_1
| vertical_1_1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',covered_1_1) ).
cnf(c0,plain,
vertical_1_1,
inference(resolution,[status(thm)],[covered_1_1,uncovered3_1_2]) ).
cnf(unique_cover5_2_1,negated_conjecture,
( ~ vertical_2_1
| ~ vertical_1_1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover5_2_1) ).
cnf(c6,plain,
~ vertical_2_1,
inference(resolution,[status(thm)],[unique_cover5_2_1,c0]) ).
cnf(covered_3_1,negated_conjecture,
( horizontal_3_1
| vertical_3_1
| vertical_2_1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',covered_3_1) ).
cnf(c32,plain,
( horizontal_3_1
| vertical_3_1 ),
inference(resolution,[status(thm)],[covered_3_1,c6]) ).
cnf(c163,plain,
( horizontal_3_1
| ~ vertical_4_1 ),
inference(resolution,[status(thm)],[c32,unique_cover5_4_1]) ).
cnf(c189,plain,
( horizontal_3_1
| horizontal_5_1 ),
inference(resolution,[status(thm)],[c163,covered_5_1]) ).
cnf(c205,plain,
( horizontal_5_1
| ~ vertical_3_2 ),
inference(resolution,[status(thm)],[c189,unique_cover4_3_2]) ).
cnf(covered_4_2,negated_conjecture,
( horizontal_4_2
| vertical_4_2
| horizontal_4_1
| vertical_3_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',covered_4_2) ).
cnf(unique_cover1_4_1,negated_conjecture,
( ~ horizontal_4_1
| ~ vertical_4_1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover1_4_1) ).
cnf(c79,plain,
( ~ horizontal_4_1
| horizontal_5_1 ),
inference(resolution,[status(thm)],[unique_cover1_4_1,covered_5_1]) ).
cnf(c166,plain,
( horizontal_5_1
| horizontal_4_2
| vertical_4_2
| vertical_3_2 ),
inference(resolution,[status(thm)],[c79,covered_4_2]) ).
cnf(c659,plain,
( horizontal_5_1
| horizontal_4_2
| vertical_4_2 ),
inference(resolution,[status(thm)],[c166,c205]) ).
cnf(unique_cover6_4_3,negated_conjecture,
( ~ horizontal_4_2
| ~ vertical_3_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover6_4_3) ).
cnf(unique_cover1_3_1,negated_conjecture,
( ~ horizontal_3_1
| ~ vertical_3_1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover1_3_1) ).
cnf(unique_cover4_2_3,negated_conjecture,
( ~ vertical_2_3
| ~ horizontal_2_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover4_2_3) ).
cnf(unique_cover6_3_2,negated_conjecture,
( ~ horizontal_3_1
| ~ vertical_2_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover6_3_2) ).
cnf(uncovered2_1_2,negated_conjecture,
~ vertical_1_2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',uncovered2_1_2) ).
cnf(unique_cover3_2_1,negated_conjecture,
( ~ horizontal_2_1
| ~ vertical_1_1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover3_2_1) ).
cnf(c5,plain,
~ horizontal_2_1,
inference(resolution,[status(thm)],[unique_cover3_2_1,c0]) ).
cnf(covered_2_2,negated_conjecture,
( horizontal_2_2
| vertical_2_2
| horizontal_2_1
| vertical_1_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',covered_2_2) ).
cnf(c7,plain,
( horizontal_2_2
| vertical_2_2
| vertical_1_2 ),
inference(resolution,[status(thm)],[covered_2_2,c5]) ).
cnf(c184,plain,
( horizontal_2_2
| vertical_2_2 ),
inference(resolution,[status(thm)],[c7,uncovered2_1_2]) ).
cnf(c201,plain,
( horizontal_2_2
| ~ horizontal_3_1 ),
inference(resolution,[status(thm)],[c184,unique_cover6_3_2]) ).
cnf(c213,plain,
( horizontal_2_2
| vertical_3_1 ),
inference(resolution,[status(thm)],[c201,c32]) ).
cnf(c235,plain,
( vertical_3_1
| ~ vertical_2_3 ),
inference(resolution,[status(thm)],[c213,unique_cover4_2_3]) ).
cnf(covered_3_3,negated_conjecture,
( horizontal_3_3
| vertical_3_3
| horizontal_3_2
| vertical_2_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',covered_3_3) ).
cnf(unique_cover2_3_2,negated_conjecture,
( ~ horizontal_3_2
| ~ horizontal_3_1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover2_3_2) ).
cnf(c159,plain,
( vertical_3_1
| ~ horizontal_3_2 ),
inference(resolution,[status(thm)],[c32,unique_cover2_3_2]) ).
cnf(c176,plain,
( vertical_3_1
| horizontal_3_3
| vertical_3_3
| vertical_2_3 ),
inference(resolution,[status(thm)],[c159,covered_3_3]) ).
cnf(c737,plain,
( vertical_3_1
| horizontal_3_3
| vertical_3_3 ),
inference(resolution,[status(thm)],[c176,c235]) ).
cnf(c745,plain,
( horizontal_3_3
| vertical_3_3
| ~ horizontal_3_1 ),
inference(resolution,[status(thm)],[c737,unique_cover1_3_1]) ).
cnf(c764,plain,
( horizontal_3_3
| vertical_3_3
| horizontal_5_1 ),
inference(resolution,[status(thm)],[c745,c189]) ).
cnf(c808,plain,
( horizontal_3_3
| horizontal_5_1
| ~ horizontal_4_2 ),
inference(resolution,[status(thm)],[c764,unique_cover6_4_3]) ).
cnf(c884,plain,
( horizontal_3_3
| horizontal_5_1
| vertical_4_2 ),
inference(resolution,[status(thm)],[c808,c659]) ).
cnf(c904,plain,
( horizontal_3_3
| horizontal_5_1
| ~ horizontal_5_2 ),
inference(resolution,[status(thm)],[c884,unique_cover3_5_2]) ).
cnf(unique_cover5_4_3,negated_conjecture,
( ~ vertical_4_3
| ~ vertical_3_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover5_4_3) ).
cnf(c806,plain,
( horizontal_3_3
| horizontal_5_1
| ~ vertical_4_3 ),
inference(resolution,[status(thm)],[c764,unique_cover5_4_3]) ).
cnf(c851,plain,
( horizontal_3_3
| horizontal_5_1
| horizontal_5_2
| vertical_4_5 ),
inference(resolution,[status(thm)],[c806,c286]) ).
cnf(c3779,plain,
( horizontal_3_3
| horizontal_5_1
| vertical_4_5 ),
inference(resolution,[status(thm)],[c851,c904]) ).
cnf(c3807,plain,
( horizontal_3_3
| vertical_4_5
| vertical_4_3 ),
inference(resolution,[status(thm)],[c3779,c480]) ).
cnf(c3880,plain,
( horizontal_3_3
| vertical_4_5
| ~ horizontal_5_3 ),
inference(resolution,[status(thm)],[c3807,unique_cover3_5_3]) ).
cnf(c169,plain,
( vertical_4_1
| horizontal_5_3
| vertical_4_3 ),
inference(resolution,[status(thm)],[c130,covered_5_3]) ).
cnf(c304,plain,
( horizontal_5_3
| vertical_4_3
| ~ horizontal_5_1 ),
inference(resolution,[status(thm)],[c169,unique_cover3_5_1]) ).
cnf(c854,plain,
( horizontal_3_3
| horizontal_5_1
| horizontal_5_3
| horizontal_5_2 ),
inference(resolution,[status(thm)],[c806,covered_5_3]) ).
cnf(c4327,plain,
( horizontal_3_3
| horizontal_5_1
| horizontal_5_3 ),
inference(resolution,[status(thm)],[c854,c904]) ).
cnf(c4353,plain,
( horizontal_3_3
| horizontal_5_3
| vertical_4_3 ),
inference(resolution,[status(thm)],[c4327,c304]) ).
cnf(unique_cover1_3_2,negated_conjecture,
( ~ horizontal_3_2
| ~ vertical_3_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover1_3_2) ).
cnf(c206,plain,
( horizontal_3_1
| ~ horizontal_5_2 ),
inference(resolution,[status(thm)],[c189,unique_cover2_5_2]) ).
cnf(c234,plain,
( horizontal_3_1
| horizontal_5_3
| vertical_4_3 ),
inference(resolution,[status(thm)],[c206,covered_5_3]) ).
cnf(unique_cover4_4_3,negated_conjecture,
( ~ vertical_4_3
| ~ horizontal_4_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover4_4_3) ).
cnf(unique_cover3_4_1,negated_conjecture,
( ~ horizontal_4_1
| ~ vertical_3_1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover3_4_1) ).
cnf(c161,plain,
( horizontal_3_1
| ~ horizontal_4_1 ),
inference(resolution,[status(thm)],[c32,unique_cover3_4_1]) ).
cnf(unique_cover6_5_2,negated_conjecture,
( ~ horizontal_5_1
| ~ vertical_4_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover6_5_2) ).
cnf(c134,plain,
( ~ horizontal_5_1
| horizontal_4_2
| horizontal_4_1
| vertical_3_2 ),
inference(resolution,[status(thm)],[unique_cover6_5_2,covered_4_2]) ).
cnf(c619,plain,
( horizontal_4_2
| horizontal_4_1
| vertical_3_2
| horizontal_3_1 ),
inference(resolution,[status(thm)],[c134,c189]) ).
cnf(c2132,plain,
( horizontal_4_2
| vertical_3_2
| horizontal_3_1 ),
inference(resolution,[status(thm)],[c619,c161]) ).
cnf(c2188,plain,
( vertical_3_2
| horizontal_3_1
| ~ vertical_4_3 ),
inference(resolution,[status(thm)],[c2132,unique_cover4_4_3]) ).
cnf(c2215,plain,
( vertical_3_2
| horizontal_3_1
| horizontal_5_3 ),
inference(resolution,[status(thm)],[c2188,c234]) ).
cnf(c758,plain,
( vertical_3_1
| horizontal_3_3
| ~ vertical_4_3 ),
inference(resolution,[status(thm)],[c737,unique_cover5_4_3]) ).
cnf(c789,plain,
( vertical_3_1
| horizontal_3_3
| horizontal_5_3
| horizontal_5_2 ),
inference(resolution,[status(thm)],[c758,covered_5_3]) ).
cnf(c4349,plain,
( horizontal_3_3
| horizontal_5_3
| ~ horizontal_5_2 ),
inference(resolution,[status(thm)],[c4327,unique_cover2_5_2]) ).
cnf(c4418,plain,
( horizontal_3_3
| horizontal_5_3
| vertical_3_1 ),
inference(resolution,[status(thm)],[c4349,c789]) ).
cnf(c4469,plain,
( horizontal_3_3
| horizontal_5_3
| ~ horizontal_3_1 ),
inference(resolution,[status(thm)],[c4418,unique_cover1_3_1]) ).
cnf(c4689,plain,
( horizontal_3_3
| horizontal_5_3
| vertical_3_2 ),
inference(resolution,[status(thm)],[c4469,c2215]) ).
cnf(c4785,plain,
( horizontal_3_3
| horizontal_5_3
| ~ horizontal_3_2 ),
inference(resolution,[status(thm)],[c4689,unique_cover1_3_2]) ).
cnf(c215,plain,
( horizontal_2_2
| horizontal_5_1 ),
inference(resolution,[status(thm)],[c201,c189]) ).
cnf(c242,plain,
( horizontal_2_2
| ~ horizontal_5_2 ),
inference(resolution,[status(thm)],[c215,unique_cover2_5_2]) ).
cnf(c256,plain,
( horizontal_2_2
| horizontal_5_3
| vertical_4_3 ),
inference(resolution,[status(thm)],[c242,covered_5_3]) ).
cnf(c237,plain,
( horizontal_2_2
| ~ horizontal_4_1 ),
inference(resolution,[status(thm)],[c213,unique_cover3_4_1]) ).
cnf(unique_cover5_3_2,negated_conjecture,
( ~ vertical_3_2
| ~ vertical_2_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover5_3_2) ).
cnf(c203,plain,
( horizontal_2_2
| ~ vertical_3_2 ),
inference(resolution,[status(thm)],[c184,unique_cover5_3_2]) ).
cnf(c217,plain,
( horizontal_2_2
| horizontal_4_2
| vertical_4_2
| horizontal_4_1 ),
inference(resolution,[status(thm)],[c203,covered_4_2]) ).
cnf(c1010,plain,
( horizontal_2_2
| horizontal_4_2
| vertical_4_2 ),
inference(resolution,[status(thm)],[c217,c237]) ).
cnf(c1031,plain,
( horizontal_2_2
| horizontal_4_2
| ~ horizontal_5_1 ),
inference(resolution,[status(thm)],[c1010,unique_cover6_5_2]) ).
cnf(c1057,plain,
( horizontal_2_2
| horizontal_4_2 ),
inference(resolution,[status(thm)],[c1031,c215]) ).
cnf(c1065,plain,
( horizontal_2_2
| ~ vertical_4_3 ),
inference(resolution,[status(thm)],[c1057,unique_cover4_4_3]) ).
cnf(c1076,plain,
( horizontal_2_2
| horizontal_5_3 ),
inference(resolution,[status(thm)],[c1065,c256]) ).
cnf(c1086,plain,
( horizontal_5_3
| ~ vertical_2_3 ),
inference(resolution,[status(thm)],[c1076,unique_cover4_2_3]) ).
cnf(c1108,plain,
( horizontal_5_3
| horizontal_3_3
| vertical_3_3
| horizontal_3_2 ),
inference(resolution,[status(thm)],[c1086,covered_3_3]) ).
cnf(c7428,plain,
( horizontal_5_3
| horizontal_3_3
| vertical_3_3 ),
inference(resolution,[status(thm)],[c1108,c4785]) ).
cnf(c7456,plain,
( horizontal_5_3
| horizontal_3_3
| ~ vertical_4_3 ),
inference(resolution,[status(thm)],[c7428,unique_cover5_4_3]) ).
cnf(c7558,plain,
( horizontal_5_3
| horizontal_3_3 ),
inference(resolution,[status(thm)],[c7456,c4353]) ).
cnf(c7570,plain,
( horizontal_3_3
| vertical_4_5 ),
inference(resolution,[status(thm)],[c7558,c3880]) ).
cnf(c7599,plain,
( vertical_4_5
| ~ horizontal_3_4 ),
inference(resolution,[status(thm)],[c7570,unique_cover2_3_4]) ).
cnf(c7660,plain,
( vertical_4_5
| vertical_3_5
| vertical_2_5 ),
inference(resolution,[status(thm)],[c7599,covered_3_5]) ).
cnf(c7964,plain,
( vertical_4_5
| vertical_2_5
| ~ horizontal_4_4 ),
inference(resolution,[status(thm)],[c7660,unique_cover6_4_5]) ).
cnf(unique_cover2_4_3,negated_conjecture,
( ~ horizontal_4_3
| ~ horizontal_4_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover2_4_3) ).
cnf(unique_cover2_5_3,negated_conjecture,
( ~ horizontal_5_3
| ~ horizontal_5_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover2_5_3) ).
cnf(c375,plain,
( vertical_4_3
| vertical_4_5
| ~ horizontal_5_3 ),
inference(resolution,[status(thm)],[c286,unique_cover2_5_3]) ).
cnf(c676,plain,
( horizontal_5_1
| horizontal_4_2
| ~ horizontal_5_2 ),
inference(resolution,[status(thm)],[c659,unique_cover3_5_2]) ).
cnf(c695,plain,
( horizontal_5_1
| horizontal_4_2
| horizontal_5_3
| vertical_4_3 ),
inference(resolution,[status(thm)],[c676,covered_5_3]) ).
cnf(c2801,plain,
( horizontal_4_2
| horizontal_5_3
| vertical_4_3 ),
inference(resolution,[status(thm)],[c695,c304]) ).
cnf(c2847,plain,
( horizontal_4_2
| vertical_4_3
| vertical_4_5 ),
inference(resolution,[status(thm)],[c2801,c375]) ).
cnf(c2878,plain,
( vertical_4_3
| vertical_4_5
| ~ horizontal_4_3 ),
inference(resolution,[status(thm)],[c2847,unique_cover2_4_3]) ).
cnf(covered_4_4,negated_conjecture,
( horizontal_4_4
| vertical_4_4
| horizontal_4_3
| vertical_3_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',covered_4_4) ).
cnf(unique_cover3_5_4,negated_conjecture,
( ~ horizontal_5_4
| ~ vertical_4_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover3_5_4) ).
cnf(c144,plain,
( ~ horizontal_5_4
| horizontal_4_4
| horizontal_4_3
| vertical_3_4 ),
inference(resolution,[status(thm)],[unique_cover3_5_4,covered_4_4]) ).
cnf(c631,plain,
( horizontal_4_4
| horizontal_4_3
| vertical_3_4
| vertical_4_5 ),
inference(resolution,[status(thm)],[c144,covered_5_5]) ).
cnf(unique_cover4_3_4,negated_conjecture,
( ~ vertical_3_4
| ~ horizontal_3_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover4_3_4) ).
cnf(c7604,plain,
( vertical_4_5
| ~ vertical_3_4 ),
inference(resolution,[status(thm)],[c7570,unique_cover4_3_4]) ).
cnf(c7688,plain,
( vertical_4_5
| horizontal_4_4
| horizontal_4_3 ),
inference(resolution,[status(thm)],[c7604,c631]) ).
cnf(c8078,plain,
( vertical_4_5
| horizontal_4_4
| vertical_4_3 ),
inference(resolution,[status(thm)],[c7688,c2878]) ).
cnf(unique_cover1_4_3,negated_conjecture,
( ~ horizontal_4_3
| ~ vertical_4_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover1_4_3) ).
cnf(c2891,plain,
( horizontal_4_2
| vertical_4_5
| ~ horizontal_4_3 ),
inference(resolution,[status(thm)],[c2847,unique_cover1_4_3]) ).
cnf(c8076,plain,
( vertical_4_5
| horizontal_4_4
| horizontal_4_2 ),
inference(resolution,[status(thm)],[c7688,c2891]) ).
cnf(c8573,plain,
( vertical_4_5
| horizontal_4_4
| ~ vertical_4_3 ),
inference(resolution,[status(thm)],[c8076,unique_cover4_4_3]) ).
cnf(c9249,plain,
( vertical_4_5
| horizontal_4_4 ),
inference(resolution,[status(thm)],[c8573,c8078]) ).
cnf(c9274,plain,
( vertical_4_5
| vertical_2_5 ),
inference(resolution,[status(thm)],[c9249,c7964]) ).
cnf(c9309,plain,
( vertical_2_5
| horizontal_3_4 ),
inference(resolution,[status(thm)],[c9274,c123]) ).
cnf(unique_cover1_3_4,negated_conjecture,
( ~ horizontal_3_4
| ~ vertical_3_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover1_3_4) ).
cnf(c7574,plain,
( horizontal_5_3
| ~ horizontal_3_4 ),
inference(resolution,[status(thm)],[c7558,unique_cover2_3_4]) ).
cnf(c7614,plain,
( horizontal_5_3
| vertical_3_5
| vertical_2_5 ),
inference(resolution,[status(thm)],[c7574,covered_3_5]) ).
cnf(c7843,plain,
( horizontal_5_3
| vertical_2_5
| ~ vertical_4_5 ),
inference(resolution,[status(thm)],[c7614,unique_cover5_4_5]) ).
cnf(c9305,plain,
( vertical_2_5
| horizontal_5_3 ),
inference(resolution,[status(thm)],[c9274,c7843]) ).
cnf(unique_cover4_2_5,negated_conjecture,
( ~ vertical_2_5
| ~ horizontal_2_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover4_2_5) ).
cnf(c157,plain,
( horizontal_1_4
| vertical_3_5
| horizontal_3_4 ),
inference(resolution,[status(thm)],[c31,covered_3_5]) ).
cnf(c7615,plain,
( horizontal_5_3
| horizontal_1_4
| vertical_3_5 ),
inference(resolution,[status(thm)],[c7574,c157]) ).
cnf(c7871,plain,
( horizontal_5_3
| horizontal_1_4
| ~ vertical_4_5 ),
inference(resolution,[status(thm)],[c7615,unique_cover5_4_5]) ).
cnf(c7661,plain,
( vertical_4_5
| horizontal_1_4
| vertical_3_5 ),
inference(resolution,[status(thm)],[c7599,c157]) ).
cnf(c7987,plain,
( vertical_4_5
| horizontal_1_4
| ~ horizontal_4_4 ),
inference(resolution,[status(thm)],[c7661,unique_cover6_4_5]) ).
cnf(c9280,plain,
( vertical_4_5
| horizontal_1_4 ),
inference(resolution,[status(thm)],[c9249,c7987]) ).
cnf(c9319,plain,
( horizontal_1_4
| horizontal_5_3 ),
inference(resolution,[status(thm)],[c9280,c7871]) ).
cnf(c9411,plain,
( horizontal_5_3
| ~ vertical_1_5 ),
inference(resolution,[status(thm)],[c9319,unique_cover4_1_5]) ).
cnf(unique_cover2_2_3,negated_conjecture,
( ~ horizontal_2_3
| ~ horizontal_2_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover2_2_3) ).
cnf(c1088,plain,
( horizontal_5_3
| ~ horizontal_2_3 ),
inference(resolution,[status(thm)],[c1076,unique_cover2_2_3]) ).
cnf(unique_cover1_1_4,negated_conjecture,
( ~ horizontal_1_4
| ~ vertical_1_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover1_1_4) ).
cnf(covered_2_4,negated_conjecture,
( horizontal_2_4
| vertical_2_4
| horizontal_2_3
| vertical_1_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',covered_2_4) ).
cnf(c16,plain,
( horizontal_2_4
| vertical_2_4
| horizontal_2_3
| ~ horizontal_1_4 ),
inference(resolution,[status(thm)],[covered_2_4,unique_cover1_1_4]) ).
cnf(c264,plain,
( horizontal_2_4
| vertical_2_4
| horizontal_2_3
| vertical_1_5 ),
inference(resolution,[status(thm)],[c16,covered_1_5]) ).
cnf(c1313,plain,
( horizontal_2_4
| vertical_2_4
| vertical_1_5
| horizontal_5_3 ),
inference(resolution,[status(thm)],[c264,c1088]) ).
cnf(c10803,plain,
( horizontal_2_4
| vertical_2_4
| horizontal_5_3 ),
inference(resolution,[status(thm)],[c1313,c9411]) ).
cnf(c10817,plain,
( vertical_2_4
| horizontal_5_3
| ~ vertical_2_5 ),
inference(resolution,[status(thm)],[c10803,unique_cover4_2_5]) ).
cnf(c10843,plain,
( vertical_2_4
| horizontal_5_3 ),
inference(resolution,[status(thm)],[c10817,c9305]) ).
cnf(c10852,plain,
( horizontal_5_3
| ~ horizontal_3_3 ),
inference(resolution,[status(thm)],[c10843,unique_cover6_3_4]) ).
cnf(c10900,plain,
horizontal_5_3,
inference(resolution,[status(thm)],[c10852,c7558]) ).
cnf(c10907,plain,
~ horizontal_5_4,
inference(resolution,[status(thm)],[c10900,unique_cover2_5_4]) ).
cnf(c10915,plain,
vertical_4_5,
inference(resolution,[status(thm)],[c10907,covered_5_5]) ).
cnf(unique_cover4_4_5,negated_conjecture,
( ~ vertical_4_5
| ~ horizontal_4_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover4_4_5) ).
cnf(unique_cover6_5_4,negated_conjecture,
( ~ horizontal_5_3
| ~ vertical_4_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover6_5_4) ).
cnf(c145,plain,
( ~ horizontal_5_3
| horizontal_4_4
| horizontal_4_3
| vertical_3_4 ),
inference(resolution,[status(thm)],[unique_cover6_5_4,covered_4_4]) ).
cnf(c10905,plain,
( horizontal_4_4
| horizontal_4_3
| vertical_3_4 ),
inference(resolution,[status(thm)],[c10900,c145]) ).
cnf(c11043,plain,
( horizontal_4_3
| vertical_3_4
| ~ vertical_4_5 ),
inference(resolution,[status(thm)],[c10905,unique_cover4_4_5]) ).
cnf(c11202,plain,
( horizontal_4_3
| vertical_3_4 ),
inference(resolution,[status(thm)],[c11043,c10915]) ).
cnf(unique_cover3_4_3,negated_conjecture,
( ~ horizontal_4_3
| ~ vertical_3_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover3_4_3) ).
cnf(unique_cover3_4_2,negated_conjecture,
( ~ horizontal_4_2
| ~ vertical_3_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover3_4_2) ).
cnf(c2189,plain,
( vertical_3_2
| horizontal_3_1
| ~ horizontal_4_3 ),
inference(resolution,[status(thm)],[c2132,unique_cover2_4_3]) ).
cnf(c11206,plain,
( vertical_3_4
| vertical_3_2
| horizontal_3_1 ),
inference(resolution,[status(thm)],[c11202,c2189]) ).
cnf(c236,plain,
( vertical_3_1
| ~ horizontal_2_3 ),
inference(resolution,[status(thm)],[c213,unique_cover2_2_3]) ).
cnf(c245,plain,
( vertical_3_1
| horizontal_2_4
| vertical_2_4
| vertical_1_4 ),
inference(resolution,[status(thm)],[c236,covered_2_4]) ).
cnf(c1138,plain,
( vertical_3_1
| horizontal_2_4
| vertical_2_4
| ~ horizontal_1_4 ),
inference(resolution,[status(thm)],[c245,unique_cover1_1_4]) ).
cnf(c271,plain,
( horizontal_3_4
| vertical_2_5
| horizontal_5_4 ),
inference(resolution,[status(thm)],[c123,covered_5_5]) ).
cnf(c368,plain,
( horizontal_3_4
| horizontal_5_4
| horizontal_1_4 ),
inference(resolution,[status(thm)],[c271,c31]) ).
cnf(c747,plain,
( vertical_3_1
| vertical_3_3
| ~ horizontal_3_4 ),
inference(resolution,[status(thm)],[c737,unique_cover2_3_4]) ).
cnf(c776,plain,
( vertical_3_1
| vertical_3_3
| horizontal_5_4
| horizontal_1_4 ),
inference(resolution,[status(thm)],[c747,c368]) ).
cnf(unique_cover6_5_5,negated_conjecture,
( ~ horizontal_5_4
| ~ vertical_4_5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover6_5_5) ).
cnf(c9317,plain,
( horizontal_1_4
| ~ horizontal_5_4 ),
inference(resolution,[status(thm)],[c9280,unique_cover6_5_5]) ).
cnf(c9398,plain,
( horizontal_1_4
| vertical_3_1
| vertical_3_3 ),
inference(resolution,[status(thm)],[c9317,c776]) ).
cnf(c9676,plain,
( horizontal_1_4
| vertical_3_1
| ~ horizontal_4_3 ),
inference(resolution,[status(thm)],[c9398,unique_cover3_4_3]) ).
cnf(c296,plain,
( horizontal_1_4
| horizontal_3_4
| ~ vertical_4_5 ),
inference(resolution,[status(thm)],[c157,unique_cover5_4_5]) ).
cnf(c9321,plain,
( horizontal_1_4
| horizontal_3_4 ),
inference(resolution,[status(thm)],[c9280,c296]) ).
cnf(c11224,plain,
( horizontal_4_3
| ~ horizontal_3_4 ),
inference(resolution,[status(thm)],[c11202,unique_cover1_3_4]) ).
cnf(c11280,plain,
( horizontal_4_3
| horizontal_1_4 ),
inference(resolution,[status(thm)],[c11224,c9321]) ).
cnf(c11309,plain,
( horizontal_1_4
| vertical_3_1 ),
inference(resolution,[status(thm)],[c11280,c9676]) ).
cnf(c11367,plain,
( vertical_3_1
| horizontal_2_4
| vertical_2_4 ),
inference(resolution,[status(thm)],[c11309,c1138]) ).
cnf(unique_cover3_2_4,negated_conjecture,
( ~ horizontal_2_4
| ~ vertical_1_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover3_2_4) ).
cnf(c1124,plain,
( vertical_3_1
| vertical_2_4
| vertical_1_4
| ~ vertical_2_5 ),
inference(resolution,[status(thm)],[c245,unique_cover4_2_5]) ).
cnf(c774,plain,
( vertical_3_1
| vertical_3_3
| vertical_2_5
| horizontal_5_4 ),
inference(resolution,[status(thm)],[c747,c271]) ).
cnf(c9306,plain,
( vertical_2_5
| ~ horizontal_5_4 ),
inference(resolution,[status(thm)],[c9274,unique_cover6_5_5]) ).
cnf(c9345,plain,
( vertical_2_5
| vertical_3_1
| vertical_3_3 ),
inference(resolution,[status(thm)],[c9306,c774]) ).
cnf(c9632,plain,
( vertical_2_5
| vertical_3_1
| ~ horizontal_4_3 ),
inference(resolution,[status(thm)],[c9345,unique_cover3_4_3]) ).
cnf(c11278,plain,
( horizontal_4_3
| vertical_2_5 ),
inference(resolution,[status(thm)],[c11224,c9309]) ).
cnf(c11290,plain,
( vertical_2_5
| vertical_3_1 ),
inference(resolution,[status(thm)],[c11278,c9632]) ).
cnf(c11337,plain,
( vertical_3_1
| vertical_2_4
| vertical_1_4 ),
inference(resolution,[status(thm)],[c11290,c1124]) ).
cnf(c11919,plain,
( vertical_3_1
| vertical_2_4
| ~ horizontal_2_4 ),
inference(resolution,[status(thm)],[c11337,unique_cover3_2_4]) ).
cnf(c12361,plain,
( vertical_3_1
| vertical_2_4 ),
inference(resolution,[status(thm)],[c11919,c11367]) ).
cnf(c12373,plain,
( vertical_3_1
| ~ horizontal_3_3 ),
inference(resolution,[status(thm)],[c12361,unique_cover6_3_4]) ).
cnf(c757,plain,
( vertical_3_1
| horizontal_3_3
| ~ horizontal_4_3 ),
inference(resolution,[status(thm)],[c737,unique_cover3_4_3]) ).
cnf(c11216,plain,
( vertical_3_4
| vertical_3_1
| horizontal_3_3 ),
inference(resolution,[status(thm)],[c11202,c757]) ).
cnf(unique_cover5_3_4,negated_conjecture,
( ~ vertical_3_4
| ~ vertical_2_4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover5_3_4) ).
cnf(c12372,plain,
( vertical_3_1
| ~ vertical_3_4 ),
inference(resolution,[status(thm)],[c12361,unique_cover5_3_4]) ).
cnf(c12413,plain,
( vertical_3_1
| horizontal_3_3 ),
inference(resolution,[status(thm)],[c12372,c11216]) ).
cnf(c12452,plain,
vertical_3_1,
inference(resolution,[status(thm)],[c12413,c12373]) ).
cnf(c12459,plain,
~ horizontal_3_1,
inference(resolution,[status(thm)],[c12452,unique_cover1_3_1]) ).
cnf(c12474,plain,
( vertical_3_4
| vertical_3_2 ),
inference(resolution,[status(thm)],[c12459,c11206]) ).
cnf(c12502,plain,
( vertical_3_4
| ~ horizontal_4_2 ),
inference(resolution,[status(thm)],[c12474,unique_cover3_4_2]) ).
cnf(c1058,plain,
( horizontal_4_2
| ~ vertical_2_3 ),
inference(resolution,[status(thm)],[c1057,unique_cover4_2_3]) ).
cnf(c1072,plain,
( horizontal_4_2
| horizontal_3_3
| vertical_3_3
| horizontal_3_2 ),
inference(resolution,[status(thm)],[c1058,covered_3_3]) ).
cnf(c12469,plain,
( horizontal_4_2
| vertical_3_2 ),
inference(resolution,[status(thm)],[c12459,c2132]) ).
cnf(c12490,plain,
( horizontal_4_2
| ~ horizontal_3_2 ),
inference(resolution,[status(thm)],[c12469,unique_cover1_3_2]) ).
cnf(c12562,plain,
( horizontal_4_2
| horizontal_3_3
| vertical_3_3 ),
inference(resolution,[status(thm)],[c12490,c1072]) ).
cnf(c12655,plain,
( horizontal_3_3
| vertical_3_3
| vertical_3_4 ),
inference(resolution,[status(thm)],[c12562,c12502]) ).
cnf(c12733,plain,
( horizontal_3_3
| vertical_3_4
| ~ horizontal_4_3 ),
inference(resolution,[status(thm)],[c12655,unique_cover3_4_3]) ).
cnf(c12864,plain,
( horizontal_3_3
| vertical_3_4 ),
inference(resolution,[status(thm)],[c12733,c11202]) ).
cnf(c12868,plain,
( vertical_3_4
| ~ horizontal_3_4 ),
inference(resolution,[status(thm)],[c12864,unique_cover2_3_4]) ).
cnf(c12888,plain,
( vertical_3_4
| vertical_2_5 ),
inference(resolution,[status(thm)],[c12868,c9309]) ).
cnf(c12917,plain,
( vertical_2_5
| ~ horizontal_3_4 ),
inference(resolution,[status(thm)],[c12888,unique_cover1_3_4]) ).
cnf(c12971,plain,
vertical_2_5,
inference(resolution,[status(thm)],[c12917,c9309]) ).
cnf(c12976,plain,
horizontal_1_4,
inference(resolution,[status(thm)],[c12971,c31]) ).
cnf(c12981,plain,
~ vertical_1_5,
inference(resolution,[status(thm)],[c12976,unique_cover4_1_5]) ).
cnf(c1298,plain,
( vertical_2_4
| horizontal_2_3
| vertical_1_5
| ~ vertical_2_5 ),
inference(resolution,[status(thm)],[c264,unique_cover4_2_5]) ).
cnf(c12978,plain,
( vertical_2_4
| horizontal_2_3
| vertical_1_5 ),
inference(resolution,[status(thm)],[c12971,c1298]) ).
cnf(c13059,plain,
( vertical_2_4
| horizontal_2_3 ),
inference(resolution,[status(thm)],[c12978,c12981]) ).
cnf(c13062,plain,
( horizontal_2_3
| ~ horizontal_3_3 ),
inference(resolution,[status(thm)],[c13059,unique_cover6_3_4]) ).
cnf(c13061,plain,
( horizontal_2_3
| ~ vertical_3_4 ),
inference(resolution,[status(thm)],[c13059,unique_cover5_3_4]) ).
cnf(c13078,plain,
( horizontal_2_3
| horizontal_3_3 ),
inference(resolution,[status(thm)],[c13061,c12864]) ).
cnf(c13162,plain,
horizontal_2_3,
inference(resolution,[status(thm)],[c13078,c13062]) ).
cnf(unique_cover1_2_3,negated_conjecture,
( ~ horizontal_2_3
| ~ vertical_2_3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover1_2_3) ).
cnf(unique_cover3_3_2,negated_conjecture,
( ~ horizontal_3_2
| ~ vertical_2_2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_cover3_3_2) ).
cnf(c200,plain,
( horizontal_2_2
| ~ horizontal_3_2 ),
inference(resolution,[status(thm)],[c184,unique_cover3_3_2]) ).
cnf(c211,plain,
( horizontal_2_2
| horizontal_3_3
| vertical_3_3
| vertical_2_3 ),
inference(resolution,[status(thm)],[c200,covered_3_3]) ).
cnf(c984,plain,
( horizontal_2_2
| horizontal_3_3
| vertical_2_3
| ~ horizontal_4_2 ),
inference(resolution,[status(thm)],[c211,unique_cover6_4_3]) ).
cnf(c5725,plain,
( horizontal_2_2
| horizontal_3_3
| vertical_2_3 ),
inference(resolution,[status(thm)],[c984,c1057]) ).
cnf(c5745,plain,
( horizontal_2_2
| vertical_2_3
| ~ vertical_3_4 ),
inference(resolution,[status(thm)],[c5725,unique_cover4_3_4]) ).
cnf(c376,plain,
( vertical_4_3
| vertical_4_5
| horizontal_2_2 ),
inference(resolution,[status(thm)],[c286,c242]) ).
cnf(c1083,plain,
( horizontal_2_2
| vertical_4_5 ),
inference(resolution,[status(thm)],[c1065,c376]) ).
cnf(c1066,plain,
( horizontal_2_2
| ~ horizontal_4_3 ),
inference(resolution,[status(thm)],[c1057,unique_cover2_4_3]) ).
cnf(c1092,plain,
( horizontal_2_2
| horizontal_4_4
| horizontal_4_3
| vertical_3_4 ),
inference(resolution,[status(thm)],[c1076,c145]) ).
cnf(c6384,plain,
( horizontal_2_2
| horizontal_4_4
| vertical_3_4 ),
inference(resolution,[status(thm)],[c1092,c1066]) ).
cnf(c6427,plain,
( horizontal_2_2
| vertical_3_4
| ~ vertical_4_5 ),
inference(resolution,[status(thm)],[c6384,unique_cover4_4_5]) ).
cnf(c6495,plain,
( horizontal_2_2
| vertical_3_4 ),
inference(resolution,[status(thm)],[c6427,c1083]) ).
cnf(c6519,plain,
( horizontal_2_2
| vertical_2_3 ),
inference(resolution,[status(thm)],[c6495,c5745]) ).
cnf(c6671,plain,
( vertical_2_3
| ~ horizontal_2_3 ),
inference(resolution,[status(thm)],[c6519,unique_cover2_2_3]) ).
cnf(c13165,plain,
vertical_2_3,
inference(resolution,[status(thm)],[c13162,c6671]) ).
cnf(c13179,plain,
~ horizontal_2_3,
inference(resolution,[status(thm)],[c13165,unique_cover1_2_3]) ).
cnf(c13204,plain,
$false,
inference(resolution,[status(thm)],[c13179,c13162]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : PUZ016-2.005 : TPTP v8.1.2. Released v1.2.0.
% 0.03/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %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 : 300
% 0.12/0.33 % DateTime : Wed May 8 20:41:22 EDT 2024
% 0.12/0.33 % CPUTime :
% 6.49/6.66 % Version: 1.5
% 6.49/6.66 % SZS status Unsatisfiable
% 6.49/6.66 % SZS output start CNFRefutation
% See solution above
% 6.49/6.66
% 6.49/6.66 % Initial clauses : 117
% 6.49/6.66 % Processed clauses : 938
% 6.49/6.66 % Factors computed : 0
% 6.49/6.66 % Resolvents computed: 13205
% 6.49/6.66 % Tautologies deleted: 218
% 6.49/6.66 % Forward subsumed : 1707
% 6.49/6.66 % Backward subsumed : 863
% 6.49/6.66 % -------- CPU Time ---------
% 6.49/6.66 % User time : 6.279 s
% 6.49/6.66 % System time : 0.045 s
% 6.49/6.66 % Total time : 6.324 s
%------------------------------------------------------------------------------