%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : ALG067+1 : TPTP v8.1.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n020.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 : Thu Jul 14 17:21:37 EDT 2022
% Result : Theorem 0.39s 1.40s
% Output : Proof 0.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : ALG067+1 : TPTP v8.1.0. Released v2.7.0.
% 0.11/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n020.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 : 600
% 0.12/0.33 % DateTime : Wed Jun 8 00:40:21 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.39/1.40 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/1.41 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/1.42
% 0.39/1.42 %-----------------------------------------------------
% 0.39/1.42 fof(co1, conjecture, ~ (((! op(e0, e0)) = e0 | op(e0, e0) = e0) & ((! op(e0, e0)) = e1 | op(e0, e1) = e0) & ((! op(e0, e0)) = e2 | op(e0, e2) = e0) & ((! op(e0, e0)) = e3 | op(e0, e3) = e0) & ((! op(e0, e0)) = e4 | op(e0, e4) = e0) & ((! op(e1, e1)) = e0 | op(e1, e0) = e1) & ((! op(e1, e1)) = e1 | op(e1, e1) = e1) & ((! op(e1, e1)) = e2 | op(e1, e2) = e1) & ((! op(e1, e1)) = e3 | op(e1, e3) = e1) & ((! op(e1, e1)) = e4 | op(e1, e4) = e1) & ((! op(e2, e2)) = e0 | op(e2, e0) = e2) & ((! op(e2, e2)) = e1 | op(e2, e1) = e2) & ((! op(e2, e2)) = e2 | op(e2, e2) = e2) & ((! op(e2, e2)) = e3 | op(e2, e3) = e2) & ((! op(e2, e2)) = e4 | op(e2, e4) = e2) & ((! op(e3, e3)) = e0 | op(e3, e0) = e3) & ((! op(e3, e3)) = e1 | op(e3, e1) = e3) & ((! op(e3, e3)) = e2 | op(e3, e2) = e3) & ((! op(e3, e3)) = e3 | op(e3, e3) = e3) & ((! op(e3, e3)) = e4 | op(e3, e4) = e3) & ((! op(e4, e4)) = e0 | op(e4, e0) = e4) & ((! op(e4, e4)) = e1 | op(e4, e1) = e4) & ((! op(e4, e4)) = e2 | op(e4, e2) = e4) & ((! op(e4, e4)) = e3 | op(e4, e3) = e4) & ((! op(e4, e4)) = e4 | op(e4, e4) = e4) & (op(e0, e0) = e0 & op(e0, e0) = e0 & (! op(e0, e0)) = e0 | op(e0, e0) = e1 & op(e1, e1) = e0 & (! op(e0, e1)) = e0 | op(e0, e0) = e2 & op(e2, e2) = e0 & (! op(e0, e2)) = e0 | op(e0, e0) = e3 & op(e3, e3) = e0 & (! op(e0, e3)) = e0 | op(e0, e0) = e4 & op(e4, e4) = e0 & (! op(e0, e4)) = e0 | op(e1, e1) = e0 & op(e0, e0) = e1 & (! op(e1, e0)) = e1 | op(e1, e1) = e1 & op(e1, e1) = e1 & (! op(e1, e1)) = e1 | op(e1, e1) = e2 & op(e2, e2) = e1 & (! op(e1, e2)) = e1 | op(e1, e1) = e3 & op(e3, e3) = e1 & (! op(e1, e3)) = e1 | op(e1, e1) = e4 & op(e4, e4) = e1 & (! op(e1, e4)) = e1 | op(e2, e2) = e0 & op(e0, e0) = e2 & (! op(e2, e0)) = e2 | op(e2, e2) = e1 & op(e1, e1) = e2 & (! op(e2, e1)) = e2 | op(e2, e2) = e2 & op(e2, e2) = e2 & (! op(e2, e2)) = e2 | op(e2, e2) = e3 & op(e3, e3) = e2 & (! op(e2, e3)) = e2 | op(e2, e2) = e4 & op(e4, e4) = e2 & (! op(e2, e4)) = e2 | op(e3, e3) = e0 & op(e0, e0) = e3 & (! op(e3, e0)) = e3 | op(e3, e3) = e1 & op(e1, e1) = e3 & (! op(e3, e1)) = e3 | op(e3, e3) = e2 & op(e2, e2) = e3 & (! op(e3, e2)) = e3 | op(e3, e3) = e3 & op(e3, e3) = e3 & (! op(e3, e3)) = e3 | op(e3, e3) = e4 & op(e4, e4) = e3 & (! op(e3, e4)) = e3 | op(e4, e4) = e0 & op(e0, e0) = e4 & (! op(e4, e0)) = e4 | op(e4, e4) = e1 & op(e1, e1) = e4 & (! op(e4, e1)) = e4 | op(e4, e4) = e2 & op(e2, e2) = e4 & (! op(e4, e2)) = e4 | op(e4, e4) = e3 & op(e3, e3) = e4 & (! op(e4, e3)) = e4 | op(e4, e4) = e4 & op(e4, e4) = e4 & (! op(e4, e4)) = e4)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 0.39/1.42
% 0.39/1.42 cnf(1, plain, [-(25 ^ []), op(e4, e4) = e4], clausify(co1)).
% 0.39/1.42 cnf(2, plain, [-(25 ^ []), -(op(e4, e4) = e4)], clausify(co1)).
% 0.39/1.42 cnf(3, plain, [-(24 ^ []), op(e4, e3) = e4], clausify(co1)).
% 0.39/1.42 cnf(4, plain, [-(24 ^ []), -(op(e4, e4) = e3)], clausify(co1)).
% 0.39/1.42 cnf(5, plain, [-(23 ^ []), op(e4, e2) = e4], clausify(co1)).
% 0.39/1.42 cnf(6, plain, [-(23 ^ []), -(op(e4, e4) = e2)], clausify(co1)).
% 0.39/1.42 cnf(7, plain, [-(22 ^ []), op(e4, e1) = e4], clausify(co1)).
% 0.39/1.42 cnf(8, plain, [-(22 ^ []), -(op(e4, e4) = e1)], clausify(co1)).
% 0.39/1.42 cnf(9, plain, [-(21 ^ []), op(e4, e0) = e4], clausify(co1)).
% 0.39/1.42 cnf(10, plain, [-(21 ^ []), -(op(e4, e4) = e0)], clausify(co1)).
% 0.39/1.42 cnf(11, plain, [-(20 ^ []), op(e3, e4) = e3], clausify(co1)).
% 0.39/1.42 cnf(12, plain, [-(20 ^ []), -(op(e3, e3) = e4)], clausify(co1)).
% 0.39/1.42 cnf(13, plain, [-(19 ^ []), op(e3, e3) = e3], clausify(co1)).
% 0.39/1.42 cnf(14, plain, [-(19 ^ []), -(op(e3, e3) = e3)], clausify(co1)).
% 0.39/1.42 cnf(15, plain, [-(18 ^ []), op(e3, e2) = e3], clausify(co1)).
% 0.39/1.42 cnf(16, plain, [-(18 ^ []), -(op(e3, e3) = e2)], clausify(co1)).
% 0.39/1.42 cnf(17, plain, [-(17 ^ []), op(e3, e1) = e3], clausify(co1)).
% 0.39/1.42 cnf(18, plain, [-(17 ^ []), -(op(e3, e3) = e1)], clausify(co1)).
% 0.39/1.42 cnf(19, plain, [-(16 ^ []), op(e3, e0) = e3], clausify(co1)).
% 0.39/1.42 cnf(20, plain, [-(16 ^ []), -(op(e3, e3) = e0)], clausify(co1)).
% 0.39/1.42 cnf(21, plain, [-(15 ^ []), op(e2, e4) = e2], clausify(co1)).
% 0.39/1.42 cnf(22, plain, [-(15 ^ []), -(op(e2, e2) = e4)], clausify(co1)).
% 0.39/1.42 cnf(23, plain, [-(14 ^ []), op(e2, e3) = e2], clausify(co1)).
% 0.39/1.42 cnf(24, plain, [-(14 ^ []), -(op(e2, e2) = e3)], clausify(co1)).
% 0.39/1.42 cnf(25, plain, [-(13 ^ []), op(e2, e2) = e2], clausify(co1)).
% 0.39/1.42 cnf(26, plain, [-(13 ^ []), -(op(e2, e2) = e2)], clausify(co1)).
% 0.39/1.42 cnf(27, plain, [-(12 ^ []), op(e2, e1) = e2], clausify(co1)).
% 0.39/1.42 cnf(28, plain, [-(12 ^ []), -(op(e2, e2) = e1)], clausify(co1)).
% 0.39/1.42 cnf(29, plain, [-(11 ^ []), op(e2, e0) = e2], clausify(co1)).
% 0.39/1.42 cnf(30, plain, [-(11 ^ []), -(op(e2, e2) = e0)], clausify(co1)).
% 0.39/1.42 cnf(31, plain, [-(10 ^ []), op(e1, e4) = e1], clausify(co1)).
% 0.39/1.42 cnf(32, plain, [-(10 ^ []), -(op(e1, e1) = e4)], clausify(co1)).
% 0.39/1.42 cnf(33, plain, [-(9 ^ []), op(e1, e3) = e1], clausify(co1)).
% 0.39/1.42 cnf(34, plain, [-(9 ^ []), -(op(e1, e1) = e3)], clausify(co1)).
% 0.39/1.42 cnf(35, plain, [-(8 ^ []), op(e1, e2) = e1], clausify(co1)).
% 0.39/1.42 cnf(36, plain, [-(8 ^ []), -(op(e1, e1) = e2)], clausify(co1)).
% 0.39/1.42 cnf(37, plain, [-(7 ^ []), op(e1, e1) = e1], clausify(co1)).
% 0.39/1.42 cnf(38, plain, [-(7 ^ []), -(op(e1, e1) = e1)], clausify(co1)).
% 0.39/1.42 cnf(39, plain, [-(6 ^ []), op(e1, e0) = e1], clausify(co1)).
% 0.39/1.42 cnf(40, plain, [-(6 ^ []), -(op(e1, e1) = e0)], clausify(co1)).
% 0.39/1.42 cnf(41, plain, [-(5 ^ []), op(e0, e4) = e0], clausify(co1)).
% 0.39/1.42 cnf(42, plain, [-(5 ^ []), -(op(e0, e0) = e4)], clausify(co1)).
% 0.39/1.42 cnf(43, plain, [-(4 ^ []), op(e0, e3) = e0], clausify(co1)).
% 0.39/1.42 cnf(44, plain, [-(4 ^ []), -(op(e0, e0) = e3)], clausify(co1)).
% 0.39/1.42 cnf(45, plain, [-(3 ^ []), op(e0, e2) = e0], clausify(co1)).
% 0.39/1.42 cnf(46, plain, [-(3 ^ []), -(op(e0, e0) = e2)], clausify(co1)).
% 0.39/1.42 cnf(47, plain, [-(2 ^ []), op(e0, e1) = e0], clausify(co1)).
% 0.39/1.42 cnf(48, plain, [-(2 ^ []), -(op(e0, e0) = e1)], clausify(co1)).
% 0.39/1.42 cnf(49, plain, [-(1 ^ []), op(e0, e0) = e0], clausify(co1)).
% 0.39/1.42 cnf(50, plain, [-(1 ^ []), -(op(e0, e0) = e0)], clausify(co1)).
% 0.39/1.42 cnf(51, plain, [op(e0, e0) = e1, -(op(e0, e1) = e0)], clausify(co1)).
% 0.39/1.42 cnf(52, plain, [op(e0, e0) = e2, -(op(e0, e2) = e0)], clausify(co1)).
% 0.39/1.42 cnf(53, plain, [op(e0, e0) = e3, -(op(e0, e3) = e0)], clausify(co1)).
% 0.39/1.42 cnf(54, plain, [op(e0, e0) = e4, -(op(e0, e4) = e0)], clausify(co1)).
% 0.39/1.42 cnf(55, plain, [op(e1, e1) = e0, -(op(e1, e0) = e1)], clausify(co1)).
% 0.39/1.42 cnf(56, plain, [op(e1, e1) = e2, -(op(e1, e2) = e1)], clausify(co1)).
% 0.39/1.42 cnf(57, plain, [op(e1, e1) = e3, -(op(e1, e3) = e1)], clausify(co1)).
% 0.39/1.42 cnf(58, plain, [op(e1, e1) = e4, -(op(e1, e4) = e1)], clausify(co1)).
% 0.39/1.42 cnf(59, plain, [op(e2, e2) = e0, -(op(e2, e0) = e2)], clausify(co1)).
% 0.39/1.42 cnf(60, plain, [op(e2, e2) = e1, -(op(e2, e1) = e2)], clausify(co1)).
% 0.39/1.42 cnf(61, plain, [op(e2, e2) = e3, -(op(e2, e3) = e2)], clausify(co1)).
% 0.39/1.42 cnf(62, plain, [op(e2, e2) = e4, -(op(e2, e4) = e2)], clausify(co1)).
% 0.39/1.42 cnf(63, plain, [op(e3, e3) = e0, -(op(e3, e0) = e3)], clausify(co1)).
% 0.39/1.42 cnf(64, plain, [op(e3, e3) = e1, -(op(e3, e1) = e3)], clausify(co1)).
% 0.39/1.42 cnf(65, plain, [op(e3, e3) = e2, -(op(e3, e2) = e3)], clausify(co1)).
% 0.39/1.42 cnf(66, plain, [op(e3, e3) = e4, -(op(e3, e4) = e3)], clausify(co1)).
% 0.39/1.42 cnf(67, plain, [op(e4, e4) = e0, -(op(e4, e0) = e4)], clausify(co1)).
% 0.39/1.42 cnf(68, plain, [op(e4, e4) = e1, -(op(e4, e1) = e4)], clausify(co1)).
% 0.39/1.42 cnf(69, plain, [op(e4, e4) = e2, -(op(e4, e2) = e4)], clausify(co1)).
% 0.39/1.42 cnf(70, plain, [op(e4, e4) = e3, -(op(e4, e3) = e4)], clausify(co1)).
% 0.39/1.42 cnf(71, plain, [1 ^ [], 2 ^ [], 3 ^ [], 4 ^ [], 5 ^ [], 6 ^ [], 7 ^ [], 8 ^ [], 9 ^ [], 10 ^ [], 11 ^ [], 12 ^ [], 13 ^ [], 14 ^ [], 15 ^ [], 16 ^ [], 17 ^ [], 18 ^ [], 19 ^ [], 20 ^ [], 21 ^ [], 22 ^ [], 23 ^ [], 24 ^ [], 25 ^ []], clausify(co1)).
% 0.39/1.42
% 0.39/1.42 cnf('1',plain,[1 ^ [], 2 ^ [], 3 ^ [], 4 ^ [], 5 ^ [], 6 ^ [], 7 ^ [], 8 ^ [], 9 ^ [], 10 ^ [], 11 ^ [], 12 ^ [], 13 ^ [], 14 ^ [], 15 ^ [], 16 ^ [], 17 ^ [], 18 ^ [], 19 ^ [], 20 ^ [], 21 ^ [], 22 ^ [], 23 ^ [], 24 ^ [], 25 ^ []],start(71)).
% 0.39/1.42 cnf('1.1',plain,[-(1 ^ []), op(e0, e0) = e0],extension(49)).
% 0.39/1.42 cnf('1.1.1',plain,[-(op(e0, e0) = e0), -(1 ^ [])],extension(50)).
% 0.39/1.42 cnf('1.1.1.1',plain,[1 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.2',plain,[-(2 ^ []), op(e0, e1) = e0],extension(47)).
% 0.39/1.42 cnf('1.2.1',plain,[-(op(e0, e1) = e0), op(e0, e0) = e1],extension(51)).
% 0.39/1.42 cnf('1.2.1.1',plain,[-(op(e0, e0) = e1), -(2 ^ [])],extension(48)).
% 0.39/1.42 cnf('1.2.1.1.1',plain,[2 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.3',plain,[-(3 ^ []), op(e0, e2) = e0],extension(45)).
% 0.39/1.42 cnf('1.3.1',plain,[-(op(e0, e2) = e0), op(e0, e0) = e2],extension(52)).
% 0.39/1.42 cnf('1.3.1.1',plain,[-(op(e0, e0) = e2), -(3 ^ [])],extension(46)).
% 0.39/1.42 cnf('1.3.1.1.1',plain,[3 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.4',plain,[-(4 ^ []), op(e0, e3) = e0],extension(43)).
% 0.39/1.42 cnf('1.4.1',plain,[-(op(e0, e3) = e0), op(e0, e0) = e3],extension(53)).
% 0.39/1.42 cnf('1.4.1.1',plain,[-(op(e0, e0) = e3), -(4 ^ [])],extension(44)).
% 0.39/1.42 cnf('1.4.1.1.1',plain,[4 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.5',plain,[-(5 ^ []), op(e0, e4) = e0],extension(41)).
% 0.39/1.42 cnf('1.5.1',plain,[-(op(e0, e4) = e0), op(e0, e0) = e4],extension(54)).
% 0.39/1.42 cnf('1.5.1.1',plain,[-(op(e0, e0) = e4), -(5 ^ [])],extension(42)).
% 0.39/1.42 cnf('1.5.1.1.1',plain,[5 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.6',plain,[-(6 ^ []), op(e1, e0) = e1],extension(39)).
% 0.39/1.42 cnf('1.6.1',plain,[-(op(e1, e0) = e1), op(e1, e1) = e0],extension(55)).
% 0.39/1.42 cnf('1.6.1.1',plain,[-(op(e1, e1) = e0), -(6 ^ [])],extension(40)).
% 0.39/1.42 cnf('1.6.1.1.1',plain,[6 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.7',plain,[-(7 ^ []), op(e1, e1) = e1],extension(37)).
% 0.39/1.42 cnf('1.7.1',plain,[-(op(e1, e1) = e1), -(7 ^ [])],extension(38)).
% 0.39/1.42 cnf('1.7.1.1',plain,[7 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.8',plain,[-(8 ^ []), op(e1, e2) = e1],extension(35)).
% 0.39/1.42 cnf('1.8.1',plain,[-(op(e1, e2) = e1), op(e1, e1) = e2],extension(56)).
% 0.39/1.42 cnf('1.8.1.1',plain,[-(op(e1, e1) = e2), -(8 ^ [])],extension(36)).
% 0.39/1.42 cnf('1.8.1.1.1',plain,[8 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.9',plain,[-(9 ^ []), op(e1, e3) = e1],extension(33)).
% 0.39/1.42 cnf('1.9.1',plain,[-(op(e1, e3) = e1), op(e1, e1) = e3],extension(57)).
% 0.39/1.42 cnf('1.9.1.1',plain,[-(op(e1, e1) = e3), -(9 ^ [])],extension(34)).
% 0.39/1.42 cnf('1.9.1.1.1',plain,[9 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.10',plain,[-(10 ^ []), op(e1, e4) = e1],extension(31)).
% 0.39/1.42 cnf('1.10.1',plain,[-(op(e1, e4) = e1), op(e1, e1) = e4],extension(58)).
% 0.39/1.42 cnf('1.10.1.1',plain,[-(op(e1, e1) = e4), -(10 ^ [])],extension(32)).
% 0.39/1.42 cnf('1.10.1.1.1',plain,[10 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.11',plain,[-(11 ^ []), op(e2, e0) = e2],extension(29)).
% 0.39/1.42 cnf('1.11.1',plain,[-(op(e2, e0) = e2), op(e2, e2) = e0],extension(59)).
% 0.39/1.42 cnf('1.11.1.1',plain,[-(op(e2, e2) = e0), -(11 ^ [])],extension(30)).
% 0.39/1.42 cnf('1.11.1.1.1',plain,[11 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.12',plain,[-(12 ^ []), op(e2, e1) = e2],extension(27)).
% 0.39/1.42 cnf('1.12.1',plain,[-(op(e2, e1) = e2), op(e2, e2) = e1],extension(60)).
% 0.39/1.42 cnf('1.12.1.1',plain,[-(op(e2, e2) = e1), -(12 ^ [])],extension(28)).
% 0.39/1.42 cnf('1.12.1.1.1',plain,[12 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.13',plain,[-(13 ^ []), op(e2, e2) = e2],extension(25)).
% 0.39/1.42 cnf('1.13.1',plain,[-(op(e2, e2) = e2), -(13 ^ [])],extension(26)).
% 0.39/1.42 cnf('1.13.1.1',plain,[13 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.14',plain,[-(14 ^ []), op(e2, e3) = e2],extension(23)).
% 0.39/1.42 cnf('1.14.1',plain,[-(op(e2, e3) = e2), op(e2, e2) = e3],extension(61)).
% 0.39/1.42 cnf('1.14.1.1',plain,[-(op(e2, e2) = e3), -(14 ^ [])],extension(24)).
% 0.39/1.42 cnf('1.14.1.1.1',plain,[14 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.15',plain,[-(15 ^ []), op(e2, e4) = e2],extension(21)).
% 0.39/1.42 cnf('1.15.1',plain,[-(op(e2, e4) = e2), op(e2, e2) = e4],extension(62)).
% 0.39/1.42 cnf('1.15.1.1',plain,[-(op(e2, e2) = e4), -(15 ^ [])],extension(22)).
% 0.39/1.42 cnf('1.15.1.1.1',plain,[15 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.16',plain,[-(16 ^ []), op(e3, e0) = e3],extension(19)).
% 0.39/1.42 cnf('1.16.1',plain,[-(op(e3, e0) = e3), op(e3, e3) = e0],extension(63)).
% 0.39/1.42 cnf('1.16.1.1',plain,[-(op(e3, e3) = e0), -(16 ^ [])],extension(20)).
% 0.39/1.42 cnf('1.16.1.1.1',plain,[16 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.17',plain,[-(17 ^ []), op(e3, e1) = e3],extension(17)).
% 0.39/1.42 cnf('1.17.1',plain,[-(op(e3, e1) = e3), op(e3, e3) = e1],extension(64)).
% 0.39/1.42 cnf('1.17.1.1',plain,[-(op(e3, e3) = e1), -(17 ^ [])],extension(18)).
% 0.39/1.42 cnf('1.17.1.1.1',plain,[17 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.18',plain,[-(18 ^ []), op(e3, e2) = e3],extension(15)).
% 0.39/1.42 cnf('1.18.1',plain,[-(op(e3, e2) = e3), op(e3, e3) = e2],extension(65)).
% 0.39/1.42 cnf('1.18.1.1',plain,[-(op(e3, e3) = e2), -(18 ^ [])],extension(16)).
% 0.39/1.42 cnf('1.18.1.1.1',plain,[18 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.19',plain,[-(19 ^ []), op(e3, e3) = e3],extension(13)).
% 0.39/1.42 cnf('1.19.1',plain,[-(op(e3, e3) = e3), -(19 ^ [])],extension(14)).
% 0.39/1.42 cnf('1.19.1.1',plain,[19 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.20',plain,[-(20 ^ []), op(e3, e4) = e3],extension(11)).
% 0.39/1.42 cnf('1.20.1',plain,[-(op(e3, e4) = e3), op(e3, e3) = e4],extension(66)).
% 0.39/1.42 cnf('1.20.1.1',plain,[-(op(e3, e3) = e4), -(20 ^ [])],extension(12)).
% 0.39/1.42 cnf('1.20.1.1.1',plain,[20 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.21',plain,[-(21 ^ []), op(e4, e0) = e4],extension(9)).
% 0.39/1.42 cnf('1.21.1',plain,[-(op(e4, e0) = e4), op(e4, e4) = e0],extension(67)).
% 0.39/1.42 cnf('1.21.1.1',plain,[-(op(e4, e4) = e0), -(21 ^ [])],extension(10)).
% 0.39/1.42 cnf('1.21.1.1.1',plain,[21 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.22',plain,[-(22 ^ []), op(e4, e1) = e4],extension(7)).
% 0.39/1.42 cnf('1.22.1',plain,[-(op(e4, e1) = e4), op(e4, e4) = e1],extension(68)).
% 0.39/1.42 cnf('1.22.1.1',plain,[-(op(e4, e4) = e1), -(22 ^ [])],extension(8)).
% 0.39/1.42 cnf('1.22.1.1.1',plain,[22 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.23',plain,[-(23 ^ []), op(e4, e2) = e4],extension(5)).
% 0.39/1.42 cnf('1.23.1',plain,[-(op(e4, e2) = e4), op(e4, e4) = e2],extension(69)).
% 0.39/1.42 cnf('1.23.1.1',plain,[-(op(e4, e4) = e2), -(23 ^ [])],extension(6)).
% 0.39/1.42 cnf('1.23.1.1.1',plain,[23 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.24',plain,[-(24 ^ []), op(e4, e3) = e4],extension(3)).
% 0.39/1.42 cnf('1.24.1',plain,[-(op(e4, e3) = e4), op(e4, e4) = e3],extension(70)).
% 0.39/1.42 cnf('1.24.1.1',plain,[-(op(e4, e4) = e3), -(24 ^ [])],extension(4)).
% 0.39/1.42 cnf('1.24.1.1.1',plain,[24 ^ []],reduction('1')).
% 0.39/1.42 cnf('1.25',plain,[-(25 ^ []), op(e4, e4) = e4],extension(1)).
% 0.39/1.42 cnf('1.25.1',plain,[-(op(e4, e4) = e4), -(25 ^ [])],extension(2)).
% 0.39/1.42 cnf('1.25.1.1',plain,[25 ^ []],reduction('1')).
% 0.39/1.42 %-----------------------------------------------------
% 0.39/1.42
% 0.39/1.42 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------