%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU356+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n032.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 : Tue Jul 19 12:02:14 EDT 2022
% Result : Theorem 30.43s 30.25s
% Output : Proof 30.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : SEU356+1 : TPTP v8.1.0. Released v3.3.0.
% 0.00/0.09 % Command : leancop_casc.sh %s %d
% 0.09/0.28 % Computer : n032.cluster.edu
% 0.09/0.28 % Model : x86_64 x86_64
% 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.28 % Memory : 8042.1875MB
% 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.28 % CPULimit : 300
% 0.09/0.28 % WCLimit : 600
% 0.09/0.28 % DateTime : Sun Jun 19 00:32:17 EDT 2022
% 0.09/0.28 % CPUTime :
% 30.43/30.25 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 30.43/30.25 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 30.43/30.26
% 30.43/30.26 %-----------------------------------------------------
% 30.43/30.26 fof(t15_yellow_0, conjecture, ! [_45951] : (antisymmetric_relstr(_45951) & rel_str(_45951) => ! [_45973] : (ex_sup_of_relstr_set(_45951, _45973) <=> ? [_45991] : (element(_45991, the_carrier(_45951)) & relstr_set_smaller(_45951, _45973, _45991) & ! [_46026] : (element(_46026, the_carrier(_45951)) => relstr_set_smaller(_45951, _45973, _46026) => related(_45951, _45991, _46026))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t15_yellow_0)).
% 30.43/30.26 fof(d7_yellow_0, axiom, ! [_46457] : (rel_str(_46457) => ! [_46472] : (ex_sup_of_relstr_set(_46457, _46472) <=> ? [_46490] : (element(_46490, the_carrier(_46457)) & relstr_set_smaller(_46457, _46472, _46490) & ! [_46525] : (element(_46525, the_carrier(_46457)) => relstr_set_smaller(_46457, _46472, _46525) => related(_46457, _46490, _46525)) & ! [_46525] : (element(_46525, the_carrier(_46457)) => relstr_set_smaller(_46457, _46472, _46525) & ! [_46607] : (element(_46607, the_carrier(_46457)) => relstr_set_smaller(_46457, _46472, _46607) => related(_46457, _46525, _46607)) => _46525 = _46490)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d7_yellow_0)).
% 30.43/30.26 fof(t25_orders_2, axiom, ! [_47301] : (antisymmetric_relstr(_47301) & rel_str(_47301) => ! [_47323] : (element(_47323, the_carrier(_47301)) => ! [_47345] : (element(_47345, the_carrier(_47301)) => related(_47301, _47323, _47345) & related(_47301, _47345, _47323) => _47323 = _47345))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t25_orders_2)).
% 30.43/30.26
% 30.43/30.26 cnf(1, plain, [-(19 ^ []), element(_20764, the_carrier(13 ^ [])), relstr_set_smaller(13 ^ [], 14 ^ [], _20764), -(related(13 ^ [], 18 ^ [], _20764))], clausify(t15_yellow_0)).
% 30.43/30.26 cnf(2, plain, [-(19 ^ []), -(relstr_set_smaller(13 ^ [], 14 ^ [], 18 ^ []))], clausify(t15_yellow_0)).
% 30.43/30.26 cnf(3, plain, [-(19 ^ []), -(element(18 ^ [], the_carrier(13 ^ [])))], clausify(t15_yellow_0)).
% 30.43/30.26 cnf(4, plain, [-(19 ^ []), ex_sup_of_relstr_set(13 ^ [], 14 ^ [])], clausify(t15_yellow_0)).
% 30.43/30.26 cnf(5, plain, [-(16 ^ [_20548]), related(13 ^ [], _20548, 15 ^ [_20548])], clausify(t15_yellow_0)).
% 30.43/30.26 cnf(6, plain, [-(16 ^ [_20548]), -(relstr_set_smaller(13 ^ [], 14 ^ [], 15 ^ [_20548]))], clausify(t15_yellow_0)).
% 30.43/30.26 cnf(7, plain, [-(16 ^ [_20548]), -(element(15 ^ [_20548], the_carrier(13 ^ [])))], clausify(t15_yellow_0)).
% 30.43/30.26 cnf(8, plain, [-(17 ^ []), element(_20548, the_carrier(13 ^ [])), relstr_set_smaller(13 ^ [], 14 ^ [], _20548), 16 ^ [_20548]], clausify(t15_yellow_0)).
% 30.43/30.26 cnf(9, plain, [-(17 ^ []), -(ex_sup_of_relstr_set(13 ^ [], 14 ^ []))], clausify(t15_yellow_0)).
% 30.43/30.26 cnf(10, plain, [-(8 ^ [_13443, _13245, _13063]), element(_19685, the_carrier(_13063)), relstr_set_smaller(_13063, _13245, _19685), -(related(_13063, 7 ^ [_13443, _13245, _13063], _19685))], clausify(d7_yellow_0)).
% 30.43/30.26 cnf(11, plain, [-(8 ^ [_13443, _13245, _13063]), -(relstr_set_smaller(_13063, _13245, 7 ^ [_13443, _13245, _13063]))], clausify(d7_yellow_0)).
% 30.43/30.26 cnf(12, plain, [-(8 ^ [_13443, _13245, _13063]), 7 ^ [_13443, _13245, _13063] = _13443], clausify(d7_yellow_0)).
% 30.43/30.26 cnf(13, plain, [-(8 ^ [_13443, _13245, _13063]), -(element(7 ^ [_13443, _13245, _13063], the_carrier(_13063)))], clausify(d7_yellow_0)).
% 30.43/30.26 cnf(14, plain, [-(6 ^ [_13443, _13245, _13063]), related(_13063, _13443, 5 ^ [_13443, _13245, _13063])], clausify(d7_yellow_0)).
% 30.43/30.26 cnf(15, plain, [-(6 ^ [_13443, _13245, _13063]), -(relstr_set_smaller(_13063, _13245, 5 ^ [_13443, _13245, _13063]))], clausify(d7_yellow_0)).
% 30.43/30.26 cnf(16, plain, [-(6 ^ [_13443, _13245, _13063]), -(element(5 ^ [_13443, _13245, _13063], the_carrier(_13063)))], clausify(d7_yellow_0)).
% 30.43/30.26 cnf(17, plain, [-(4 ^ [_13245, _13063]), element(_19274, the_carrier(_13063)), relstr_set_smaller(_13063, _13245, _19274), -(related(_13063, 1 ^ [_13245, _13063], _19274))], clausify(d7_yellow_0)).
% 30.43/30.26 cnf(18, plain, [-(4 ^ [_13245, _13063]), -(relstr_set_smaller(_13063, _13245, 1 ^ [_13245, _13063]))], clausify(d7_yellow_0)).
% 30.43/30.26 cnf(19, plain, [-(4 ^ [_13245, _13063]), -(element(1 ^ [_13245, _13063], the_carrier(_13063)))], clausify(d7_yellow_0)).
% 30.43/30.26 cnf(20, plain, [-(9 ^ [_13063]), ex_sup_of_relstr_set(_13063, _13245), 4 ^ [_13245, _13063]], clausify(d7_yellow_0)).
% 30.43/30.26 cnf(21, plain, [-(9 ^ [_13063]), -(ex_sup_of_relstr_set(_13063, _13245)), element(_13443, the_carrier(_13063)), relstr_set_smaller(_13063, _13245, _13443), 6 ^ [_13443, _13245, _13063], 8 ^ [_13443, _13245, _13063]], clausify(d7_yellow_0)).
% 30.43/30.26 cnf(22, plain, [-(antisymmetric_relstr(13 ^ []))], clausify(t15_yellow_0)).
% 30.43/30.26 cnf(23, plain, [-(rel_str(13 ^ []))], clausify(t15_yellow_0)).
% 30.43/30.26 cnf(24, plain, [17 ^ [], 19 ^ []], clausify(t15_yellow_0)).
% 30.43/30.26 cnf(25, plain, [rel_str(_13063), 9 ^ [_13063]], clausify(d7_yellow_0)).
% 30.43/30.26 cnf(26, plain, [rel_str(_16169), antisymmetric_relstr(_16169), element(_16344, the_carrier(_16169)), element(_16492, the_carrier(_16169)), -(_16344 = _16492), related(_16169, _16344, _16492), related(_16169, _16492, _16344)], clausify(t25_orders_2)).
% 30.43/30.26
% 30.43/30.26 cnf('1',plain,[17 ^ [], 19 ^ []],start(24)).
% 30.43/30.26 cnf('1.1',plain,[-(17 ^ []), -(ex_sup_of_relstr_set(13 ^ [], 14 ^ []))],extension(9)).
% 30.43/30.26 cnf('1.1.1',plain,[ex_sup_of_relstr_set(13 ^ [], 14 ^ []), -(9 ^ [13 ^ []]), 4 ^ [14 ^ [], 13 ^ []]],extension(20,bind([[_13245, _13063], [14 ^ [], 13 ^ []]]))).
% 30.43/30.26 cnf('1.1.1.1',plain,[9 ^ [13 ^ []], rel_str(13 ^ [])],extension(25,bind([[_13063], [13 ^ []]]))).
% 30.43/30.26 cnf('1.1.1.1.1',plain,[-(rel_str(13 ^ []))],extension(23)).
% 30.43/30.26 cnf('1.1.1.2',plain,[-(4 ^ [14 ^ [], 13 ^ []]), element(15 ^ [1 ^ [14 ^ [], 13 ^ []]], the_carrier(13 ^ [])), relstr_set_smaller(13 ^ [], 14 ^ [], 15 ^ [1 ^ [14 ^ [], 13 ^ []]]), -(related(13 ^ [], 1 ^ [14 ^ [], 13 ^ []], 15 ^ [1 ^ [14 ^ [], 13 ^ []]]))],extension(17,bind([[_13245, _13063, _19274], [14 ^ [], 13 ^ [], 15 ^ [1 ^ [14 ^ [], 13 ^ []]]]]))).
% 30.43/30.26 cnf('1.1.1.2.1',plain,[-(element(15 ^ [1 ^ [14 ^ [], 13 ^ []]], the_carrier(13 ^ []))), -(16 ^ [1 ^ [14 ^ [], 13 ^ []]])],extension(7,bind([[_20548], [1 ^ [14 ^ [], 13 ^ []]]]))).
% 30.43/30.26 cnf('1.1.1.2.1.1',plain,[16 ^ [1 ^ [14 ^ [], 13 ^ []]], -(17 ^ []), element(1 ^ [14 ^ [], 13 ^ []], the_carrier(13 ^ [])), relstr_set_smaller(13 ^ [], 14 ^ [], 1 ^ [14 ^ [], 13 ^ []])],extension(8,bind([[_20548], [1 ^ [14 ^ [], 13 ^ []]]]))).
% 30.43/30.26 cnf('1.1.1.2.1.1.1',plain,[17 ^ []],reduction('1')).
% 30.43/30.26 cnf('1.1.1.2.1.1.2',plain,[-(element(1 ^ [14 ^ [], 13 ^ []], the_carrier(13 ^ []))), -(4 ^ [14 ^ [], 13 ^ []])],extension(19,bind([[_13245, _13063], [14 ^ [], 13 ^ []]]))).
% 30.43/30.26 cnf('1.1.1.2.1.1.2.1',plain,[4 ^ [14 ^ [], 13 ^ []]],reduction('1.1.1')).
% 30.43/30.26 cnf('1.1.1.2.1.1.3',plain,[-(relstr_set_smaller(13 ^ [], 14 ^ [], 1 ^ [14 ^ [], 13 ^ []])), -(4 ^ [14 ^ [], 13 ^ []])],extension(18,bind([[_13245, _13063], [14 ^ [], 13 ^ []]]))).
% 30.43/30.26 cnf('1.1.1.2.1.1.3.1',plain,[4 ^ [14 ^ [], 13 ^ []]],reduction('1.1.1')).
% 30.43/30.26 cnf('1.1.1.2.2',plain,[-(relstr_set_smaller(13 ^ [], 14 ^ [], 15 ^ [1 ^ [14 ^ [], 13 ^ []]])), -(16 ^ [1 ^ [14 ^ [], 13 ^ []]])],extension(6,bind([[_20548], [1 ^ [14 ^ [], 13 ^ []]]]))).
% 30.43/30.26 cnf('1.1.1.2.2.1',plain,[16 ^ [1 ^ [14 ^ [], 13 ^ []]], -(17 ^ []), element(1 ^ [14 ^ [], 13 ^ []], the_carrier(13 ^ [])), relstr_set_smaller(13 ^ [], 14 ^ [], 1 ^ [14 ^ [], 13 ^ []])],extension(8,bind([[_20548], [1 ^ [14 ^ [], 13 ^ []]]]))).
% 30.43/30.26 cnf('1.1.1.2.2.1.1',plain,[17 ^ []],reduction('1')).
% 30.43/30.26 cnf('1.1.1.2.2.1.2',plain,[-(element(1 ^ [14 ^ [], 13 ^ []], the_carrier(13 ^ []))), -(4 ^ [14 ^ [], 13 ^ []])],extension(19,bind([[_13245, _13063], [14 ^ [], 13 ^ []]]))).
% 30.43/30.26 cnf('1.1.1.2.2.1.2.1',plain,[4 ^ [14 ^ [], 13 ^ []]],reduction('1.1.1')).
% 30.43/30.26 cnf('1.1.1.2.2.1.3',plain,[-(relstr_set_smaller(13 ^ [], 14 ^ [], 1 ^ [14 ^ [], 13 ^ []])), -(4 ^ [14 ^ [], 13 ^ []])],extension(18,bind([[_13245, _13063], [14 ^ [], 13 ^ []]]))).
% 30.43/30.26 cnf('1.1.1.2.2.1.3.1',plain,[4 ^ [14 ^ [], 13 ^ []]],reduction('1.1.1')).
% 30.43/30.26 cnf('1.1.1.2.3',plain,[related(13 ^ [], 1 ^ [14 ^ [], 13 ^ []], 15 ^ [1 ^ [14 ^ [], 13 ^ []]]), -(16 ^ [1 ^ [14 ^ [], 13 ^ []]])],extension(5,bind([[_20548], [1 ^ [14 ^ [], 13 ^ []]]]))).
% 30.43/30.26 cnf('1.1.1.2.3.1',plain,[16 ^ [1 ^ [14 ^ [], 13 ^ []]], -(17 ^ []), element(1 ^ [14 ^ [], 13 ^ []], the_carrier(13 ^ [])), relstr_set_smaller(13 ^ [], 14 ^ [], 1 ^ [14 ^ [], 13 ^ []])],extension(8,bind([[_20548], [1 ^ [14 ^ [], 13 ^ []]]]))).
% 30.43/30.26 cnf('1.1.1.2.3.1.1',plain,[17 ^ []],reduction('1')).
% 30.43/30.26 cnf('1.1.1.2.3.1.2',plain,[-(element(1 ^ [14 ^ [], 13 ^ []], the_carrier(13 ^ []))), -(4 ^ [14 ^ [], 13 ^ []])],extension(19,bind([[_13245, _13063], [14 ^ [], 13 ^ []]]))).
% 30.43/30.26 cnf('1.1.1.2.3.1.2.1',plain,[4 ^ [14 ^ [], 13 ^ []]],reduction('1.1.1')).
% 30.43/30.26 cnf('1.1.1.2.3.1.3',plain,[-(relstr_set_smaller(13 ^ [], 14 ^ [], 1 ^ [14 ^ [], 13 ^ []])), -(4 ^ [14 ^ [], 13 ^ []])],extension(18,bind([[_13245, _13063], [14 ^ [], 13 ^ []]]))).
% 30.43/30.26 cnf('1.1.1.2.3.1.3.1',plain,[4 ^ [14 ^ [], 13 ^ []]],reduction('1.1.1')).
% 30.43/30.26 cnf('1.2',plain,[-(19 ^ []), -(relstr_set_smaller(13 ^ [], 14 ^ [], 18 ^ []))],extension(2)).
% 30.43/30.26 cnf('1.2.1',plain,[relstr_set_smaller(13 ^ [], 14 ^ [], 18 ^ []), -(8 ^ [18 ^ [], 14 ^ [], 13 ^ []]), element(18 ^ [], the_carrier(13 ^ [])), -(related(13 ^ [], 7 ^ [18 ^ [], 14 ^ [], 13 ^ []], 18 ^ []))],extension(10,bind([[_13443, _13245, _13063, _19685], [18 ^ [], 14 ^ [], 13 ^ [], 18 ^ []]]))).
% 30.43/30.26 cnf('1.2.1.1',plain,[8 ^ [18 ^ [], 14 ^ [], 13 ^ []], -(9 ^ [13 ^ []]), -(ex_sup_of_relstr_set(13 ^ [], 14 ^ [])), element(18 ^ [], the_carrier(13 ^ [])), relstr_set_smaller(13 ^ [], 14 ^ [], 18 ^ []), 6 ^ [18 ^ [], 14 ^ [], 13 ^ []]],extension(21,bind([[_13443, _13245, _13063], [18 ^ [], 14 ^ [], 13 ^ []]]))).
% 30.43/30.26 cnf('1.2.1.1.1',plain,[9 ^ [13 ^ []], rel_str(13 ^ [])],extension(25,bind([[_13063], [13 ^ []]]))).
% 30.43/30.26 cnf('1.2.1.1.1.1',plain,[-(rel_str(13 ^ []))],extension(23)).
% 30.43/30.26 cnf('1.2.1.1.2',plain,[ex_sup_of_relstr_set(13 ^ [], 14 ^ []), -(19 ^ [])],extension(4)).
% 30.43/30.26 cnf('1.2.1.1.2.1',plain,[19 ^ []],reduction('1')).
% 30.43/30.26 cnf('1.2.1.1.3',plain,[-(element(18 ^ [], the_carrier(13 ^ []))), -(19 ^ [])],extension(3)).
% 30.43/30.26 cnf('1.2.1.1.3.1',plain,[19 ^ []],reduction('1')).
% 30.43/30.26 cnf('1.2.1.1.4',plain,[-(relstr_set_smaller(13 ^ [], 14 ^ [], 18 ^ []))],reduction('1.2')).
% 30.43/30.26 cnf('1.2.1.1.5',plain,[-(6 ^ [18 ^ [], 14 ^ [], 13 ^ []]), related(13 ^ [], 18 ^ [], 5 ^ [18 ^ [], 14 ^ [], 13 ^ []])],extension(14,bind([[_13443, _13245, _13063], [18 ^ [], 14 ^ [], 13 ^ []]]))).
% 30.43/30.26 cnf('1.2.1.1.5.1',plain,[-(related(13 ^ [], 18 ^ [], 5 ^ [18 ^ [], 14 ^ [], 13 ^ []])), -(19 ^ []), element(5 ^ [18 ^ [], 14 ^ [], 13 ^ []], the_carrier(13 ^ [])), relstr_set_smaller(13 ^ [], 14 ^ [], 5 ^ [18 ^ [], 14 ^ [], 13 ^ []])],extension(1,bind([[_20764], [5 ^ [18 ^ [], 14 ^ [], 13 ^ []]]]))).
% 30.43/30.26 cnf('1.2.1.1.5.1.1',plain,[19 ^ []],reduction('1')).
% 30.43/30.26 cnf('1.2.1.1.5.1.2',plain,[-(element(5 ^ [18 ^ [], 14 ^ [], 13 ^ []], the_carrier(13 ^ []))), -(6 ^ [18 ^ [], 14 ^ [], 13 ^ []])],extension(16,bind([[_13443, _13245, _13063], [18 ^ [], 14 ^ [], 13 ^ []]]))).
% 30.43/30.26 cnf('1.2.1.1.5.1.2.1',plain,[6 ^ [18 ^ [], 14 ^ [], 13 ^ []]],reduction('1.2.1.1')).
% 30.43/30.26 cnf('1.2.1.1.5.1.3',plain,[-(relstr_set_smaller(13 ^ [], 14 ^ [], 5 ^ [18 ^ [], 14 ^ [], 13 ^ []])), -(6 ^ [18 ^ [], 14 ^ [], 13 ^ []])],extension(15,bind([[_13443, _13245, _13063], [18 ^ [], 14 ^ [], 13 ^ []]]))).
% 30.43/30.26 cnf('1.2.1.1.5.1.3.1',plain,[6 ^ [18 ^ [], 14 ^ [], 13 ^ []]],reduction('1.2.1.1')).
% 30.43/30.26 cnf('1.2.1.2',plain,[-(element(18 ^ [], the_carrier(13 ^ []))), -(19 ^ [])],extension(3)).
% 30.43/30.26 cnf('1.2.1.2.1',plain,[19 ^ []],reduction('1')).
% 30.43/30.26 cnf('1.2.1.3',plain,[related(13 ^ [], 7 ^ [18 ^ [], 14 ^ [], 13 ^ []], 18 ^ []), rel_str(13 ^ []), antisymmetric_relstr(13 ^ []), element(7 ^ [18 ^ [], 14 ^ [], 13 ^ []], the_carrier(13 ^ [])), element(18 ^ [], the_carrier(13 ^ [])), -(7 ^ [18 ^ [], 14 ^ [], 13 ^ []] = 18 ^ []), related(13 ^ [], 18 ^ [], 7 ^ [18 ^ [], 14 ^ [], 13 ^ []])],extension(26,bind([[_16169, _16492, _16344], [13 ^ [], 18 ^ [], 7 ^ [18 ^ [], 14 ^ [], 13 ^ []]]]))).
% 30.43/30.26 cnf('1.2.1.3.1',plain,[-(rel_str(13 ^ []))],extension(23)).
% 30.43/30.26 cnf('1.2.1.3.2',plain,[-(antisymmetric_relstr(13 ^ []))],extension(22)).
% 30.43/30.26 cnf('1.2.1.3.3',plain,[-(element(7 ^ [18 ^ [], 14 ^ [], 13 ^ []], the_carrier(13 ^ []))), -(8 ^ [18 ^ [], 14 ^ [], 13 ^ []])],extension(13,bind([[_13443, _13245, _13063], [18 ^ [], 14 ^ [], 13 ^ []]]))).
% 30.43/30.26 cnf('1.2.1.3.3.1',plain,[8 ^ [18 ^ [], 14 ^ [], 13 ^ []]],lemmata('1.2.1')).
% 30.43/30.26 cnf('1.2.1.3.4',plain,[-(element(18 ^ [], the_carrier(13 ^ [])))],lemmata('1.2.1')).
% 30.43/30.26 cnf('1.2.1.3.5',plain,[7 ^ [18 ^ [], 14 ^ [], 13 ^ []] = 18 ^ [], -(8 ^ [18 ^ [], 14 ^ [], 13 ^ []])],extension(12,bind([[_13443, _13245, _13063], [18 ^ [], 14 ^ [], 13 ^ []]]))).
% 30.43/30.26 cnf('1.2.1.3.5.1',plain,[8 ^ [18 ^ [], 14 ^ [], 13 ^ []]],lemmata('1.2.1')).
% 30.43/30.26 cnf('1.2.1.3.6',plain,[-(related(13 ^ [], 18 ^ [], 7 ^ [18 ^ [], 14 ^ [], 13 ^ []])), -(19 ^ []), element(7 ^ [18 ^ [], 14 ^ [], 13 ^ []], the_carrier(13 ^ [])), relstr_set_smaller(13 ^ [], 14 ^ [], 7 ^ [18 ^ [], 14 ^ [], 13 ^ []])],extension(1,bind([[_20764], [7 ^ [18 ^ [], 14 ^ [], 13 ^ []]]]))).
% 30.43/30.26 cnf('1.2.1.3.6.1',plain,[19 ^ []],reduction('1')).
% 30.43/30.26 cnf('1.2.1.3.6.2',plain,[-(element(7 ^ [18 ^ [], 14 ^ [], 13 ^ []], the_carrier(13 ^ [])))],lemmata('1.2.1.3')).
% 30.43/30.26 cnf('1.2.1.3.6.3',plain,[-(relstr_set_smaller(13 ^ [], 14 ^ [], 7 ^ [18 ^ [], 14 ^ [], 13 ^ []])), -(8 ^ [18 ^ [], 14 ^ [], 13 ^ []])],extension(11,bind([[_13443, _13245, _13063], [18 ^ [], 14 ^ [], 13 ^ []]]))).
% 30.43/30.26 cnf('1.2.1.3.6.3.1',plain,[8 ^ [18 ^ [], 14 ^ [], 13 ^ []]],lemmata('1.2.1')).
% 30.43/30.26 %-----------------------------------------------------
% 30.43/30.26
% 30.43/30.26 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------