%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : HWV003-3 : TPTP v8.1.2. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n019.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:24:53 EDT 2024
% Result : Unsatisfiable 2.19s 2.38s
% Output : Refutation 2.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 56
% Syntax : Number of clauses : 200 ( 13 unt; 123 nHn; 200 RR)
% Number of literals : 487 ( 0 equ; 158 neg)
% Maximal clause size : 4 ( 2 avg)
% Maximal term depth : 0 ( 0 avg)
% Number of predicates : 23 ( 22 usr; 23 prp; 0-0 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_4A,negated_conjecture,
( a14
| a12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_4A) ).
cnf(clause_13A,negated_conjecture,
( a24
| cI ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_13A) ).
cnf(clause_5C,negated_conjecture,
( ~ a15
| ~ a14
| ~ cI ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_5C) ).
cnf(c22,plain,
( ~ a15
| ~ a14
| a24 ),
inference(resolution,[status(thm)],[clause_5C,clause_13A]) ).
cnf(c105,plain,
( ~ a15
| a24
| a12 ),
inference(resolution,[status(thm)],[c22,clause_4A]) ).
cnf(clause_6B,negated_conjecture,
( a16
| a15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_6B) ).
cnf(clause_7A,negated_conjecture,
( a17
| a15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_7A) ).
cnf(clause_8C,negated_conjecture,
( ~ s1
| ~ a16
| ~ a17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_8C) ).
cnf(c39,plain,
( ~ s1
| ~ a16
| a15 ),
inference(resolution,[status(thm)],[clause_8C,clause_7A]) ).
cnf(c152,plain,
( ~ s1
| a15 ),
inference(resolution,[status(thm)],[c39,clause_6B]) ).
cnf(clause_20,negated_conjecture,
( conjline18
| conjline19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_20) ).
cnf(clause_18C,negated_conjecture,
( ~ conjline18
| s1
| s2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_18C) ).
cnf(c66,plain,
( s1
| s2
| conjline19 ),
inference(resolution,[status(thm)],[clause_18C,clause_20]) ).
cnf(c283,plain,
( s2
| conjline19
| a15 ),
inference(resolution,[status(thm)],[c66,c152]) ).
cnf(clause_9A,negated_conjecture,
( c1
| a15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_9A) ).
cnf(clause_19D,negated_conjecture,
( ~ conjline19
| ~ c1
| ~ c2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_19D) ).
cnf(clause_17A,negated_conjecture,
( c2
| ~ a22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_17A) ).
cnf(clause_5B,negated_conjecture,
( a15
| cI ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_5B) ).
cnf(clause_11C,negated_conjecture,
( a22
| ~ cI
| ~ a23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_11C) ).
cnf(clause_5A,negated_conjecture,
( a15
| a14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_5A) ).
cnf(clause_2A,negated_conjecture,
( a12
| a ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2A) ).
cnf(clause_12A,negated_conjecture,
( a23
| ~ a ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_12A) ).
cnf(c16,plain,
( a23
| a12 ),
inference(resolution,[status(thm)],[clause_12A,clause_2A]) ).
cnf(clause_4C,negated_conjecture,
( ~ a14
| ~ a12
| ~ a13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_4C) ).
cnf(clause_3A,negated_conjecture,
( a13
| b ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3A) ).
cnf(clause_12B,negated_conjecture,
( a23
| ~ b ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_12B) ).
cnf(c17,plain,
( a23
| a13 ),
inference(resolution,[status(thm)],[clause_12B,clause_3A]) ).
cnf(c32,plain,
( a23
| ~ a14
| ~ a12 ),
inference(resolution,[status(thm)],[c17,clause_4C]) ).
cnf(c125,plain,
( a23
| ~ a14 ),
inference(resolution,[status(thm)],[c32,c16]) ).
cnf(c134,plain,
( a23
| a15 ),
inference(resolution,[status(thm)],[c125,clause_5A]) ).
cnf(c137,plain,
( a15
| a22
| ~ cI ),
inference(resolution,[status(thm)],[c134,clause_11C]) ).
cnf(c463,plain,
( a15
| a22 ),
inference(resolution,[status(thm)],[c137,clause_5B]) ).
cnf(c475,plain,
( a15
| c2 ),
inference(resolution,[status(thm)],[c463,clause_17A]) ).
cnf(c513,plain,
( a15
| ~ conjline19
| ~ c1 ),
inference(resolution,[status(thm)],[c475,clause_19D]) ).
cnf(c1387,plain,
( a15
| ~ conjline19 ),
inference(resolution,[status(thm)],[c513,clause_9A]) ).
cnf(c1390,plain,
( a15
| s2 ),
inference(resolution,[status(thm)],[c1387,c283]) ).
cnf(clause_16D,negated_conjecture,
( ~ s2
| ~ cI
| ~ a21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_16D) ).
cnf(clause_3B,negated_conjecture,
( a13
| a11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3B) ).
cnf(clause_1C,negated_conjecture,
( ~ a11
| ~ a
| ~ b ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1C) ).
cnf(c0,plain,
( ~ a11
| ~ a
| a13 ),
inference(resolution,[status(thm)],[clause_1C,clause_3A]) ).
cnf(c71,plain,
( ~ a11
| a13
| a12 ),
inference(resolution,[status(thm)],[c0,clause_2A]) ).
cnf(c315,plain,
( a13
| a12 ),
inference(resolution,[status(thm)],[c71,clause_3B]) ).
cnf(clause_2B,negated_conjecture,
( a12
| a11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2B) ).
cnf(clause_3C,negated_conjecture,
( ~ a13
| ~ b
| ~ a11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_3C) ).
cnf(c8,plain,
( ~ a13
| ~ b
| a12 ),
inference(resolution,[status(thm)],[clause_3C,clause_2B]) ).
cnf(clause_10B,negated_conjecture,
( a21
| ~ a
| b ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_10B) ).
cnf(c50,plain,
( a21
| b
| a12 ),
inference(resolution,[status(thm)],[clause_10B,clause_2A]) ).
cnf(c208,plain,
( a21
| a12
| ~ a13 ),
inference(resolution,[status(thm)],[c50,c8]) ).
cnf(c622,plain,
( a21
| a12 ),
inference(resolution,[status(thm)],[c208,c315]) ).
cnf(clause_2C,negated_conjecture,
( ~ a12
| ~ a
| ~ a11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_2C) ).
cnf(c3,plain,
( ~ a12
| ~ a
| a13 ),
inference(resolution,[status(thm)],[clause_2C,clause_3B]) ).
cnf(clause_10A,negated_conjecture,
( a21
| a
| ~ b ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_10A) ).
cnf(c47,plain,
( a21
| a
| a13 ),
inference(resolution,[status(thm)],[clause_10A,clause_3A]) ).
cnf(c199,plain,
( a21
| a13
| ~ a12 ),
inference(resolution,[status(thm)],[c47,c3]) ).
cnf(c585,plain,
( a21
| a13 ),
inference(resolution,[status(thm)],[c199,c315]) ).
cnf(c617,plain,
( a21
| ~ a14
| ~ a12 ),
inference(resolution,[status(thm)],[c585,clause_4C]) ).
cnf(c1565,plain,
( a21
| ~ a14 ),
inference(resolution,[status(thm)],[c617,c622]) ).
cnf(c1567,plain,
( a21
| a15 ),
inference(resolution,[status(thm)],[c1565,clause_5A]) ).
cnf(c1574,plain,
( a15
| ~ s2
| ~ cI ),
inference(resolution,[status(thm)],[c1567,clause_16D]) ).
cnf(c2603,plain,
( a15
| ~ s2 ),
inference(resolution,[status(thm)],[c1574,clause_5B]) ).
cnf(c2613,plain,
a15,
inference(resolution,[status(thm)],[c2603,c1390]) ).
cnf(c2629,plain,
( a24
| a12 ),
inference(resolution,[status(thm)],[c2613,c105]) ).
cnf(clause_13B,negated_conjecture,
( ~ a24
| ~ cI ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_13B) ).
cnf(clause_11A,negated_conjecture,
( ~ a22
| cI ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_11A) ).
cnf(clause_7C,negated_conjecture,
( ~ a17
| ~ a15
| ~ cI ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_7C) ).
cnf(c33,plain,
( ~ a17
| ~ a15
| a24 ),
inference(resolution,[status(thm)],[clause_7C,clause_13A]) ).
cnf(c2631,plain,
( ~ a17
| a24 ),
inference(resolution,[status(thm)],[c2613,c33]) ).
cnf(clause_9B,negated_conjecture,
( c1
| a11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_9B) ).
cnf(clause_17B,negated_conjecture,
( c2
| ~ a26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_17B) ).
cnf(clause_15C,negated_conjecture,
( a26
| ~ a24
| ~ a25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_15C) ).
cnf(clause_1A,negated_conjecture,
( a11
| a ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1A) ).
cnf(clause_1B,negated_conjecture,
( a11
| b ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_1B) ).
cnf(clause_14C,negated_conjecture,
( a25
| ~ a
| ~ b ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_14C) ).
cnf(c60,plain,
( a25
| ~ a
| a11 ),
inference(resolution,[status(thm)],[clause_14C,clause_1B]) ).
cnf(c235,plain,
( a25
| a11 ),
inference(resolution,[status(thm)],[c60,clause_1A]) ).
cnf(c239,plain,
( a11
| a26
| ~ a24 ),
inference(resolution,[status(thm)],[c235,clause_15C]) ).
cnf(c15,plain,
( a23
| a11 ),
inference(resolution,[status(thm)],[clause_12A,clause_1A]) ).
cnf(c54,plain,
( a22
| ~ cI
| a11 ),
inference(resolution,[status(thm)],[clause_11C,c15]) ).
cnf(c225,plain,
( a22
| a11
| a24 ),
inference(resolution,[status(thm)],[c54,clause_13A]) ).
cnf(c655,plain,
( a11
| a24
| c2 ),
inference(resolution,[status(thm)],[c225,clause_17A]) ).
cnf(c1653,plain,
( a11
| c2
| a26 ),
inference(resolution,[status(thm)],[c655,c239]) ).
cnf(c2835,plain,
( a11
| c2 ),
inference(resolution,[status(thm)],[c1653,clause_17B]) ).
cnf(c2842,plain,
( a11
| ~ conjline19
| ~ c1 ),
inference(resolution,[status(thm)],[c2835,clause_19D]) ).
cnf(c3124,plain,
( a11
| ~ conjline19 ),
inference(resolution,[status(thm)],[c2842,clause_9B]) ).
cnf(clause_10D,negated_conjecture,
( ~ a21
| ~ a
| ~ b ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_10D) ).
cnf(c52,plain,
( ~ a21
| ~ a
| a11 ),
inference(resolution,[status(thm)],[clause_10D,clause_1B]) ).
cnf(c218,plain,
( ~ a21
| a11 ),
inference(resolution,[status(thm)],[c52,clause_1A]) ).
cnf(clause_8B,negated_conjecture,
( s1
| a17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_8B) ).
cnf(clause_18D,negated_conjecture,
( ~ conjline18
| ~ s1
| ~ s2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_18D) ).
cnf(clause_7B,negated_conjecture,
( a17
| cI ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_7B) ).
cnf(clause_16B,negated_conjecture,
( s2
| ~ cI
| a21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_16B) ).
cnf(c63,plain,
( s2
| a21
| a17 ),
inference(resolution,[status(thm)],[clause_16B,clause_7B]) ).
cnf(c266,plain,
( a21
| a17
| ~ conjline18
| ~ s1 ),
inference(resolution,[status(thm)],[c63,clause_18D]) ).
cnf(c970,plain,
( a21
| a17
| ~ conjline18 ),
inference(resolution,[status(thm)],[c266,clause_8B]) ).
cnf(c1789,plain,
( a21
| a17
| conjline19 ),
inference(resolution,[status(thm)],[c970,clause_20]) ).
cnf(c2853,plain,
( a17
| conjline19
| a11 ),
inference(resolution,[status(thm)],[c1789,c218]) ).
cnf(c3145,plain,
( a17
| a11 ),
inference(resolution,[status(thm)],[c2853,c3124]) ).
cnf(c3150,plain,
( a11
| a24 ),
inference(resolution,[status(thm)],[c3145,c2631]) ).
cnf(clause_16C,negated_conjecture,
( ~ s2
| cI
| a21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_16C) ).
cnf(c287,plain,
( s1
| conjline19
| cI
| a21 ),
inference(resolution,[status(thm)],[c66,clause_16C]) ).
cnf(c38,plain,
( ~ s1
| ~ a16
| cI ),
inference(resolution,[status(thm)],[clause_8C,clause_7B]) ).
cnf(clause_6A,negated_conjecture,
( a16
| a14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_6A) ).
cnf(c1568,plain,
( a21
| a16 ),
inference(resolution,[status(thm)],[c1565,clause_6A]) ).
cnf(c1594,plain,
( a21
| ~ s1
| cI ),
inference(resolution,[status(thm)],[c1568,c38]) ).
cnf(c2802,plain,
( a21
| cI
| conjline19 ),
inference(resolution,[status(thm)],[c1594,c287]) ).
cnf(c3056,plain,
( cI
| conjline19
| a11 ),
inference(resolution,[status(thm)],[c2802,c218]) ).
cnf(c3324,plain,
( cI
| a11 ),
inference(resolution,[status(thm)],[c3056,c3124]) ).
cnf(c3330,plain,
( a11
| ~ a24 ),
inference(resolution,[status(thm)],[c3324,clause_13B]) ).
cnf(c3352,plain,
a11,
inference(resolution,[status(thm)],[c3330,c3150]) ).
cnf(c3353,plain,
( ~ a12
| ~ a ),
inference(resolution,[status(thm)],[c3352,clause_2C]) ).
cnf(clause_14A,negated_conjecture,
( ~ a25
| a ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_14A) ).
cnf(clause_15B,negated_conjecture,
( ~ a26
| a25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_15B) ).
cnf(c106,plain,
( ~ a15
| a24
| a16 ),
inference(resolution,[status(thm)],[c22,clause_6A]) ).
cnf(c370,plain,
( a24
| a16 ),
inference(resolution,[status(thm)],[c106,clause_6B]) ).
cnf(clause_4B,negated_conjecture,
( a14
| a13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_4B) ).
cnf(c24,plain,
( ~ a15
| ~ a14
| a17 ),
inference(resolution,[status(thm)],[clause_5C,clause_7B]) ).
cnf(c107,plain,
( ~ a15
| a17
| a13 ),
inference(resolution,[status(thm)],[c24,clause_4B]) ).
cnf(c390,plain,
( a17
| a13 ),
inference(resolution,[status(thm)],[c107,clause_7A]) ).
cnf(c393,plain,
( a13
| ~ s1
| ~ a16 ),
inference(resolution,[status(thm)],[c390,clause_8C]) ).
cnf(c886,plain,
( a13
| ~ s1
| a24 ),
inference(resolution,[status(thm)],[c393,c370]) ).
cnf(c103,plain,
( ~ a15
| a24
| a13 ),
inference(resolution,[status(thm)],[c22,clause_4B]) ).
cnf(c1411,plain,
( s2
| a24
| a13 ),
inference(resolution,[status(thm)],[c1390,c103]) ).
cnf(clause_16A,negated_conjecture,
( s2
| cI
| ~ a21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_16A) ).
cnf(c615,plain,
( a13
| s2
| cI ),
inference(resolution,[status(thm)],[c585,clause_16A]) ).
cnf(c1535,plain,
( a13
| s2
| ~ a24 ),
inference(resolution,[status(thm)],[c615,clause_13B]) ).
cnf(c2424,plain,
( a13
| s2 ),
inference(resolution,[status(thm)],[c1535,c1411]) ).
cnf(clause_8A,negated_conjecture,
( s1
| a16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_8A) ).
cnf(clause_6C,negated_conjecture,
( ~ a16
| ~ a14
| ~ a15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_6C) ).
cnf(c29,plain,
( ~ a16
| ~ a14
| cI ),
inference(resolution,[status(thm)],[clause_6C,clause_5B]) ).
cnf(c119,plain,
( ~ a16
| cI
| a13 ),
inference(resolution,[status(thm)],[c29,clause_4B]) ).
cnf(c422,plain,
( cI
| a13
| s1 ),
inference(resolution,[status(thm)],[c119,clause_8A]) ).
cnf(c616,plain,
( a13
| ~ s2
| ~ cI ),
inference(resolution,[status(thm)],[c585,clause_16D]) ).
cnf(c1546,plain,
( a13
| ~ s2
| s1 ),
inference(resolution,[status(thm)],[c616,c422]) ).
cnf(c2466,plain,
( a13
| s1 ),
inference(resolution,[status(thm)],[c1546,c2424]) ).
cnf(c2483,plain,
( a13
| a24 ),
inference(resolution,[status(thm)],[c2466,c886]) ).
cnf(clause_17C,negated_conjecture,
( ~ c2
| a22
| a26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_17C) ).
cnf(clause_19C,negated_conjecture,
( ~ conjline19
| c1
| c2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_19C) ).
cnf(c69,plain,
( c1
| c2
| conjline18 ),
inference(resolution,[status(thm)],[clause_19C,clause_20]) ).
cnf(clause_9C,negated_conjecture,
( ~ c1
| ~ a15
| ~ a11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_9C) ).
cnf(c42,plain,
( ~ c1
| ~ a15
| a13 ),
inference(resolution,[status(thm)],[clause_9C,clause_3B]) ).
cnf(c505,plain,
( c2
| ~ c1
| a13 ),
inference(resolution,[status(thm)],[c475,c42]) ).
cnf(c1267,plain,
( c2
| a13
| conjline18 ),
inference(resolution,[status(thm)],[c505,c69]) ).
cnf(c2453,plain,
( a13
| ~ conjline18
| ~ s1 ),
inference(resolution,[status(thm)],[c2424,clause_18D]) ).
cnf(c2960,plain,
( a13
| ~ conjline18 ),
inference(resolution,[status(thm)],[c2453,c2466]) ).
cnf(c2969,plain,
( a13
| c2 ),
inference(resolution,[status(thm)],[c2960,c1267]) ).
cnf(c2982,plain,
( a13
| a22
| a26 ),
inference(resolution,[status(thm)],[c2969,clause_17C]) ).
cnf(c3257,plain,
( a13
| a26
| cI ),
inference(resolution,[status(thm)],[c2982,clause_11A]) ).
cnf(c3463,plain,
( a13
| a26
| ~ a24 ),
inference(resolution,[status(thm)],[c3257,clause_13B]) ).
cnf(c3673,plain,
( a13
| a26 ),
inference(resolution,[status(thm)],[c3463,c2483]) ).
cnf(c3677,plain,
( a13
| a25 ),
inference(resolution,[status(thm)],[c3673,clause_15B]) ).
cnf(c3682,plain,
( a13
| a ),
inference(resolution,[status(thm)],[c3677,clause_14A]) ).
cnf(c3688,plain,
( a13
| ~ a12 ),
inference(resolution,[status(thm)],[c3682,c3353]) ).
cnf(c3701,plain,
a13,
inference(resolution,[status(thm)],[c3688,c315]) ).
cnf(c3355,plain,
( ~ a13
| ~ b ),
inference(resolution,[status(thm)],[c3352,clause_3C]) ).
cnf(clause_14B,negated_conjecture,
( ~ a25
| b ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_14B) ).
cnf(c3354,plain,
( ~ c1
| ~ a15 ),
inference(resolution,[status(thm)],[c3352,clause_9C]) ).
cnf(c3360,plain,
~ c1,
inference(resolution,[status(thm)],[c3354,c2613]) ).
cnf(c121,plain,
( ~ a16
| cI
| a12 ),
inference(resolution,[status(thm)],[c29,clause_4A]) ).
cnf(c430,plain,
( cI
| a12
| s1 ),
inference(resolution,[status(thm)],[c121,clause_8A]) ).
cnf(c1023,plain,
( a12
| s1
| ~ a24 ),
inference(resolution,[status(thm)],[c430,clause_13B]) ).
cnf(c129,plain,
( ~ a17
| a24
| a14 ),
inference(resolution,[status(thm)],[c33,clause_5A]) ).
cnf(c452,plain,
( a24
| a14
| s1 ),
inference(resolution,[status(thm)],[c129,clause_8B]) ).
cnf(c1075,plain,
( a24
| s1
| ~ a15 ),
inference(resolution,[status(thm)],[c452,c22]) ).
cnf(c2625,plain,
( a24
| s1 ),
inference(resolution,[status(thm)],[c2613,c1075]) ).
cnf(c2632,plain,
( s1
| a12 ),
inference(resolution,[status(thm)],[c2625,c1023]) ).
cnf(c632,plain,
( a12
| s2
| cI ),
inference(resolution,[status(thm)],[c622,clause_16A]) ).
cnf(c1603,plain,
( a12
| s2
| ~ a24 ),
inference(resolution,[status(thm)],[c632,clause_13B]) ).
cnf(c2812,plain,
( a12
| s2 ),
inference(resolution,[status(thm)],[c1603,c2629]) ).
cnf(c2827,plain,
( a12
| ~ conjline18
| ~ s1 ),
inference(resolution,[status(thm)],[c2812,clause_18D]) ).
cnf(c3077,plain,
( a12
| ~ conjline18 ),
inference(resolution,[status(thm)],[c2827,c2632]) ).
cnf(c3083,plain,
( a12
| conjline19 ),
inference(resolution,[status(thm)],[c3077,clause_20]) ).
cnf(clause_10C,negated_conjecture,
( ~ a21
| a
| b ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_10C) ).
cnf(c2856,plain,
( a21
| conjline19
| a24 ),
inference(resolution,[status(thm)],[c1789,c2631]) ).
cnf(c3060,plain,
( a21
| conjline19
| ~ a24 ),
inference(resolution,[status(thm)],[c2802,clause_13B]) ).
cnf(c3374,plain,
( a21
| conjline19 ),
inference(resolution,[status(thm)],[c3060,c2856]) ).
cnf(c3376,plain,
( conjline19
| a
| b ),
inference(resolution,[status(thm)],[c3374,clause_10C]) ).
cnf(c3484,plain,
( conjline19
| b
| ~ a12 ),
inference(resolution,[status(thm)],[c3376,c3353]) ).
cnf(c3786,plain,
( conjline19
| b ),
inference(resolution,[status(thm)],[c3484,c3083]) ).
cnf(c3799,plain,
( conjline19
| ~ a13 ),
inference(resolution,[status(thm)],[c3786,c3355]) ).
cnf(c3802,plain,
conjline19,
inference(resolution,[status(thm)],[c3799,c3701]) ).
cnf(c3803,plain,
( c1
| c2 ),
inference(resolution,[status(thm)],[c3802,clause_19C]) ).
cnf(c3804,plain,
c2,
inference(resolution,[status(thm)],[c3803,c3360]) ).
cnf(c3806,plain,
( a22
| a26 ),
inference(resolution,[status(thm)],[c3804,clause_17C]) ).
cnf(c3809,plain,
( a22
| a25 ),
inference(resolution,[status(thm)],[c3806,clause_15B]) ).
cnf(c3827,plain,
( a22
| b ),
inference(resolution,[status(thm)],[c3809,clause_14B]) ).
cnf(c3866,plain,
( a22
| ~ a13 ),
inference(resolution,[status(thm)],[c3827,c3355]) ).
cnf(c3936,plain,
a22,
inference(resolution,[status(thm)],[c3866,c3701]) ).
cnf(c3937,plain,
cI,
inference(resolution,[status(thm)],[c3936,clause_11A]) ).
cnf(c3939,plain,
~ a24,
inference(resolution,[status(thm)],[c3937,clause_13B]) ).
cnf(c3944,plain,
a12,
inference(resolution,[status(thm)],[c3939,c2629]) ).
cnf(clause_12C,negated_conjecture,
( ~ a23
| a
| b ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_12C) ).
cnf(clause_11B,negated_conjecture,
( ~ a22
| a23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause_11B) ).
cnf(c3807,plain,
( a26
| a23 ),
inference(resolution,[status(thm)],[c3806,clause_11B]) ).
cnf(c3811,plain,
( a23
| a25 ),
inference(resolution,[status(thm)],[c3807,clause_15B]) ).
cnf(c3835,plain,
( a23
| b ),
inference(resolution,[status(thm)],[c3811,clause_14B]) ).
cnf(c3879,plain,
( b
| a ),
inference(resolution,[status(thm)],[c3835,clause_12C]) ).
cnf(c3959,plain,
( a
| ~ a13 ),
inference(resolution,[status(thm)],[c3879,c3355]) ).
cnf(c3973,plain,
a,
inference(resolution,[status(thm)],[c3959,c3701]) ).
cnf(c3975,plain,
~ a12,
inference(resolution,[status(thm)],[c3973,c3353]) ).
cnf(c3976,plain,
$false,
inference(resolution,[status(thm)],[c3975,c3944]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : HWV003-3 : TPTP v8.1.2. Released v2.7.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.33 % Computer : n019.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.33 % DateTime : Thu May 9 07:15:23 EDT 2024
% 0.14/0.34 % CPUTime :
% 2.19/2.38 % Version: 1.5
% 2.19/2.38 % SZS status Unsatisfiable
% 2.19/2.38 % SZS output start CNFRefutation
% See solution above
% 2.19/2.38
% 2.19/2.38 % Initial clauses : 61
% 2.19/2.38 % Processed clauses : 506
% 2.19/2.38 % Factors computed : 0
% 2.19/2.38 % Resolvents computed: 3977
% 2.19/2.38 % Tautologies deleted: 97
% 2.19/2.38 % Forward subsumed : 1523
% 2.19/2.38 % Backward subsumed : 475
% 2.19/2.38 % -------- CPU Time ---------
% 2.19/2.38 % User time : 2.004 s
% 2.19/2.38 % System time : 0.016 s
% 2.19/2.38 % Total time : 2.020 s
%------------------------------------------------------------------------------