%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU190+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n005.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:00:51 EDT 2022
% Result : Theorem 29.52s 29.36s
% Output : Proof 29.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU190+1 : TPTP v8.1.0. Released v3.3.0.
% 0.07/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n005.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Mon Jun 20 06:00:08 EDT 2022
% 0.13/0.34 % CPUTime :
% 29.52/29.36 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.52/29.37 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.52/29.37
% 29.52/29.37 %-----------------------------------------------------
% 29.52/29.37 fof(d5_relat_1, axiom, ! [_61310] : (relation(_61310) => ! [_61325] : (_61325 = relation_rng(_61310) <=> ! [_61343] : (in(_61343, _61325) <=> ? [_61361] : in(ordered_pair(_61361, _61343), _61310)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d5_relat_1)).
% 29.52/29.37 fof(d4_relat_1, axiom, ! [_61652] : (relation(_61652) => ! [_61667] : (_61667 = relation_dom(_61652) <=> ! [_61685] : (in(_61685, _61667) <=> ? [_61703] : in(ordered_pair(_61685, _61703), _61652)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d4_relat_1)).
% 29.52/29.37 fof(d10_relat_1, axiom, ! [_62003, _62006] : (relation(_62006) => (_62006 = identity_relation(_62003) <=> ! [_62031, _62034] : (in(ordered_pair(_62031, _62034), _62006) <=> in(_62031, _62003) & _62031 = _62034))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d10_relat_1)).
% 29.52/29.37 fof(t71_relat_1, conjecture, ! [_62333] : (relation_dom(identity_relation(_62333)) = _62333 & relation_rng(identity_relation(_62333)) = _62333), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t71_relat_1)).
% 29.52/29.37 fof(dt_k6_relat_1, axiom, ! [_62592] : relation(identity_relation(_62592)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', dt_k6_relat_1)).
% 29.52/29.37
% 29.52/29.37 cnf(1, plain, [-(20 ^ [_20601, _20492]), in(17 ^ [_20601, _20492], _20601)], clausify(d5_relat_1)).
% 29.52/29.37 cnf(2, plain, [-(20 ^ [_20601, _20492]), -(in(ordered_pair(19 ^ [_20601, _20492], 17 ^ [_20601, _20492]), _20492))], clausify(d5_relat_1)).
% 29.52/29.37 cnf(3, plain, [-(18 ^ [_20601, _20492]), in(ordered_pair(_30801, 17 ^ [_20601, _20492]), _20492)], clausify(d5_relat_1)).
% 29.52/29.37 cnf(4, plain, [-(18 ^ [_20601, _20492]), -(in(17 ^ [_20601, _20492], _20601))], clausify(d5_relat_1)).
% 29.52/29.37 cnf(5, plain, [-(21 ^ [_20492]), -(_20601 = relation_rng(_20492)), 18 ^ [_20601, _20492], 20 ^ [_20601, _20492]], clausify(d5_relat_1)).
% 29.52/29.37 cnf(6, plain, [-(13 ^ [_19944, _19835]), in(10 ^ [_19944, _19835], _19944)], clausify(d4_relat_1)).
% 29.52/29.37 cnf(7, plain, [-(13 ^ [_19944, _19835]), -(in(ordered_pair(10 ^ [_19944, _19835], 12 ^ [_19944, _19835]), _19835))], clausify(d4_relat_1)).
% 29.52/29.37 cnf(8, plain, [-(11 ^ [_19944, _19835]), in(ordered_pair(10 ^ [_19944, _19835], _30437), _19835)], clausify(d4_relat_1)).
% 29.52/29.37 cnf(9, plain, [-(11 ^ [_19944, _19835]), -(in(10 ^ [_19944, _19835], _19944))], clausify(d4_relat_1)).
% 29.52/29.37 cnf(10, plain, [-(14 ^ [_19835]), -(_19944 = relation_dom(_19835)), 11 ^ [_19944, _19835], 13 ^ [_19944, _19835]], clausify(d4_relat_1)).
% 29.52/29.37 cnf(11, plain, [-(1 ^ [_19398, _19336, _19147, _19070]), -(_19336 = _19398)], clausify(d10_relat_1)).
% 29.52/29.37 cnf(12, plain, [-(1 ^ [_19398, _19336, _19147, _19070]), -(in(_19336, _19070))], clausify(d10_relat_1)).
% 29.52/29.37 cnf(13, plain, [-(2 ^ [_19147, _19070]), -(in(ordered_pair(_19336, _19398), _19147)), in(_19336, _19070), _19336 = _19398], clausify(d10_relat_1)).
% 29.52/29.37 cnf(14, plain, [-(2 ^ [_19147, _19070]), in(ordered_pair(_19336, _19398), _19147), 1 ^ [_19398, _19336, _19147, _19070]], clausify(d10_relat_1)).
% 29.52/29.37 cnf(15, plain, [-(7 ^ [_19147, _19070]), _19147 = identity_relation(_19070), 2 ^ [_19147, _19070]], clausify(d10_relat_1)).
% 29.52/29.37 cnf(16, plain, [relation_dom(identity_relation(32 ^ [])) = 32 ^ [], relation_rng(identity_relation(32 ^ [])) = 32 ^ []], clausify(t71_relat_1)).
% 29.52/29.37 cnf(17, plain, [_15555 = _15604, -(identity_relation(_15555) = identity_relation(_15604))], theory(equality)).
% 29.52/29.37 cnf(18, plain, [-(_12691 = _12691)], theory(equality)).
% 29.52/29.37 cnf(19, plain, [_12844 = _12889, -(_12889 = _12844)], theory(equality)).
% 29.52/29.37 cnf(20, plain, [-(in(_14619, _14750)), in(_14552, _14685), _14552 = _14619, _14685 = _14750], theory(equality)).
% 29.52/29.37 cnf(21, plain, [relation(_19147), 7 ^ [_19147, _19070]], clausify(d10_relat_1)).
% 29.52/29.37 cnf(22, plain, [relation(_19835), 14 ^ [_19835]], clausify(d4_relat_1)).
% 29.52/29.37 cnf(23, plain, [relation(_20492), 21 ^ [_20492]], clausify(d5_relat_1)).
% 29.52/29.37 cnf(24, plain, [-(relation(identity_relation(_22320)))], clausify(dt_k6_relat_1)).
% 29.52/29.37
% 29.52/29.37 cnf('1',plain,[relation_dom(identity_relation(32 ^ [])) = 32 ^ [], relation_rng(identity_relation(32 ^ [])) = 32 ^ []],start(16)).
% 29.52/29.37 cnf('1.1',plain,[-(relation_dom(identity_relation(32 ^ [])) = 32 ^ []), 32 ^ [] = relation_dom(identity_relation(32 ^ []))],extension(19,bind([[_12844, _12889], [32 ^ [], relation_dom(identity_relation(32 ^ []))]]))).
% 29.52/29.37 cnf('1.1.1',plain,[-(32 ^ [] = relation_dom(identity_relation(32 ^ []))), -(14 ^ [identity_relation(32 ^ [])]), 11 ^ [32 ^ [], identity_relation(32 ^ [])], 13 ^ [32 ^ [], identity_relation(32 ^ [])]],extension(10,bind([[_19944, _19835], [32 ^ [], identity_relation(32 ^ [])]]))).
% 29.52/29.37 cnf('1.1.1.1',plain,[14 ^ [identity_relation(32 ^ [])], relation(identity_relation(32 ^ []))],extension(22,bind([[_19835], [identity_relation(32 ^ [])]]))).
% 29.52/29.37 cnf('1.1.1.1.1',plain,[-(relation(identity_relation(32 ^ [])))],extension(24,bind([[_22320], [32 ^ []]]))).
% 29.52/29.37 cnf('1.1.1.2',plain,[-(11 ^ [32 ^ [], identity_relation(32 ^ [])]), in(ordered_pair(10 ^ [32 ^ [], identity_relation(32 ^ [])], 10 ^ [32 ^ [], identity_relation(32 ^ [])]), identity_relation(32 ^ []))],extension(8,bind([[_19944, _30437, _19835], [32 ^ [], 10 ^ [32 ^ [], identity_relation(32 ^ [])], identity_relation(32 ^ [])]]))).
% 29.52/29.37 cnf('1.1.1.2.1',plain,[-(in(ordered_pair(10 ^ [32 ^ [], identity_relation(32 ^ [])], 10 ^ [32 ^ [], identity_relation(32 ^ [])]), identity_relation(32 ^ []))), -(2 ^ [identity_relation(32 ^ []), 32 ^ []]), in(10 ^ [32 ^ [], identity_relation(32 ^ [])], 32 ^ []), 10 ^ [32 ^ [], identity_relation(32 ^ [])] = 10 ^ [32 ^ [], identity_relation(32 ^ [])]],extension(13,bind([[_19147, _19070, _19336, _19398], [identity_relation(32 ^ []), 32 ^ [], 10 ^ [32 ^ [], identity_relation(32 ^ [])], 10 ^ [32 ^ [], identity_relation(32 ^ [])]]]))).
% 29.52/29.37 cnf('1.1.1.2.1.1',plain,[2 ^ [identity_relation(32 ^ []), 32 ^ []], -(7 ^ [identity_relation(32 ^ []), 32 ^ []]), identity_relation(32 ^ []) = identity_relation(32 ^ [])],extension(15,bind([[_19147, _19070], [identity_relation(32 ^ []), 32 ^ []]]))).
% 29.52/29.37 cnf('1.1.1.2.1.1.1',plain,[7 ^ [identity_relation(32 ^ []), 32 ^ []], relation(identity_relation(32 ^ []))],extension(21,bind([[_19070, _19147], [32 ^ [], identity_relation(32 ^ [])]]))).
% 29.52/29.37 cnf('1.1.1.2.1.1.1.1',plain,[-(relation(identity_relation(32 ^ [])))],extension(24,bind([[_22320], [32 ^ []]]))).
% 29.52/29.37 cnf('1.1.1.2.1.1.2',plain,[-(identity_relation(32 ^ []) = identity_relation(32 ^ [])), 32 ^ [] = 32 ^ []],extension(17,bind([[_15555, _15604], [32 ^ [], 32 ^ []]]))).
% 29.52/29.37 cnf('1.1.1.2.1.1.2.1',plain,[-(32 ^ [] = 32 ^ [])],extension(18,bind([[_12691], [32 ^ []]]))).
% 29.52/29.37 cnf('1.1.1.2.1.2',plain,[-(in(10 ^ [32 ^ [], identity_relation(32 ^ [])], 32 ^ [])), -(11 ^ [32 ^ [], identity_relation(32 ^ [])])],extension(9,bind([[_19944, _19835], [32 ^ [], identity_relation(32 ^ [])]]))).
% 29.52/29.37 cnf('1.1.1.2.1.2.1',plain,[11 ^ [32 ^ [], identity_relation(32 ^ [])]],reduction('1.1.1')).
% 29.52/29.37 cnf('1.1.1.2.1.3',plain,[-(10 ^ [32 ^ [], identity_relation(32 ^ [])] = 10 ^ [32 ^ [], identity_relation(32 ^ [])])],extension(18,bind([[_12691], [10 ^ [32 ^ [], identity_relation(32 ^ [])]]]))).
% 29.52/29.37 cnf('1.1.1.3',plain,[-(13 ^ [32 ^ [], identity_relation(32 ^ [])]), -(in(ordered_pair(10 ^ [32 ^ [], identity_relation(32 ^ [])], 12 ^ [32 ^ [], identity_relation(32 ^ [])]), identity_relation(32 ^ [])))],extension(7,bind([[_19944, _19835], [32 ^ [], identity_relation(32 ^ [])]]))).
% 29.52/29.37 cnf('1.1.1.3.1',plain,[in(ordered_pair(10 ^ [32 ^ [], identity_relation(32 ^ [])], 12 ^ [32 ^ [], identity_relation(32 ^ [])]), identity_relation(32 ^ [])), -(2 ^ [identity_relation(32 ^ []), 32 ^ []]), 1 ^ [12 ^ [32 ^ [], identity_relation(32 ^ [])], 10 ^ [32 ^ [], identity_relation(32 ^ [])], identity_relation(32 ^ []), 32 ^ []]],extension(14,bind([[_19398, _19336, _19147, _19070], [12 ^ [32 ^ [], identity_relation(32 ^ [])], 10 ^ [32 ^ [], identity_relation(32 ^ [])], identity_relation(32 ^ []), 32 ^ []]]))).
% 29.52/29.37 cnf('1.1.1.3.1.1',plain,[2 ^ [identity_relation(32 ^ []), 32 ^ []], -(7 ^ [identity_relation(32 ^ []), 32 ^ []]), identity_relation(32 ^ []) = identity_relation(32 ^ [])],extension(15,bind([[_19147, _19070], [identity_relation(32 ^ []), 32 ^ []]]))).
% 29.52/29.37 cnf('1.1.1.3.1.1.1',plain,[7 ^ [identity_relation(32 ^ []), 32 ^ []], relation(identity_relation(32 ^ []))],extension(21,bind([[_19070, _19147], [32 ^ [], identity_relation(32 ^ [])]]))).
% 29.52/29.37 cnf('1.1.1.3.1.1.1.1',plain,[-(relation(identity_relation(32 ^ [])))],extension(24,bind([[_22320], [32 ^ []]]))).
% 29.52/29.37 cnf('1.1.1.3.1.1.2',plain,[-(identity_relation(32 ^ []) = identity_relation(32 ^ [])), 32 ^ [] = 32 ^ []],extension(17,bind([[_15555, _15604], [32 ^ [], 32 ^ []]]))).
% 29.52/29.37 cnf('1.1.1.3.1.1.2.1',plain,[-(32 ^ [] = 32 ^ [])],extension(18,bind([[_12691], [32 ^ []]]))).
% 29.52/29.37 cnf('1.1.1.3.1.2',plain,[-(1 ^ [12 ^ [32 ^ [], identity_relation(32 ^ [])], 10 ^ [32 ^ [], identity_relation(32 ^ [])], identity_relation(32 ^ []), 32 ^ []]), -(in(10 ^ [32 ^ [], identity_relation(32 ^ [])], 32 ^ []))],extension(12,bind([[_19398, _19147, _19336, _19070], [12 ^ [32 ^ [], identity_relation(32 ^ [])], identity_relation(32 ^ []), 10 ^ [32 ^ [], identity_relation(32 ^ [])], 32 ^ []]]))).
% 29.52/29.37 cnf('1.1.1.3.1.2.1',plain,[in(10 ^ [32 ^ [], identity_relation(32 ^ [])], 32 ^ []), -(13 ^ [32 ^ [], identity_relation(32 ^ [])])],extension(6,bind([[_19944, _19835], [32 ^ [], identity_relation(32 ^ [])]]))).
% 29.52/29.37 cnf('1.1.1.3.1.2.1.1',plain,[13 ^ [32 ^ [], identity_relation(32 ^ [])]],reduction('1.1.1')).
% 29.52/29.37 cnf('1.2',plain,[-(relation_rng(identity_relation(32 ^ [])) = 32 ^ []), 32 ^ [] = relation_rng(identity_relation(32 ^ []))],extension(19,bind([[_12844, _12889], [32 ^ [], relation_rng(identity_relation(32 ^ []))]]))).
% 29.52/29.37 cnf('1.2.1',plain,[-(32 ^ [] = relation_rng(identity_relation(32 ^ []))), -(21 ^ [identity_relation(32 ^ [])]), 18 ^ [32 ^ [], identity_relation(32 ^ [])], 20 ^ [32 ^ [], identity_relation(32 ^ [])]],extension(5,bind([[_20601, _20492], [32 ^ [], identity_relation(32 ^ [])]]))).
% 29.52/29.37 cnf('1.2.1.1',plain,[21 ^ [identity_relation(32 ^ [])], relation(identity_relation(32 ^ []))],extension(23,bind([[_20492], [identity_relation(32 ^ [])]]))).
% 29.52/29.37 cnf('1.2.1.1.1',plain,[-(relation(identity_relation(32 ^ [])))],extension(24,bind([[_22320], [32 ^ []]]))).
% 29.52/29.37 cnf('1.2.1.2',plain,[-(18 ^ [32 ^ [], identity_relation(32 ^ [])]), in(ordered_pair(17 ^ [32 ^ [], identity_relation(32 ^ [])], 17 ^ [32 ^ [], identity_relation(32 ^ [])]), identity_relation(32 ^ []))],extension(3,bind([[_30801, _20601, _20492], [17 ^ [32 ^ [], identity_relation(32 ^ [])], 32 ^ [], identity_relation(32 ^ [])]]))).
% 29.52/29.37 cnf('1.2.1.2.1',plain,[-(in(ordered_pair(17 ^ [32 ^ [], identity_relation(32 ^ [])], 17 ^ [32 ^ [], identity_relation(32 ^ [])]), identity_relation(32 ^ []))), -(2 ^ [identity_relation(32 ^ []), 32 ^ []]), in(17 ^ [32 ^ [], identity_relation(32 ^ [])], 32 ^ []), 17 ^ [32 ^ [], identity_relation(32 ^ [])] = 17 ^ [32 ^ [], identity_relation(32 ^ [])]],extension(13,bind([[_19147, _19070, _19336, _19398], [identity_relation(32 ^ []), 32 ^ [], 17 ^ [32 ^ [], identity_relation(32 ^ [])], 17 ^ [32 ^ [], identity_relation(32 ^ [])]]]))).
% 29.52/29.37 cnf('1.2.1.2.1.1',plain,[2 ^ [identity_relation(32 ^ []), 32 ^ []], -(7 ^ [identity_relation(32 ^ []), 32 ^ []]), identity_relation(32 ^ []) = identity_relation(32 ^ [])],extension(15,bind([[_19147, _19070], [identity_relation(32 ^ []), 32 ^ []]]))).
% 29.52/29.37 cnf('1.2.1.2.1.1.1',plain,[7 ^ [identity_relation(32 ^ []), 32 ^ []], relation(identity_relation(32 ^ []))],extension(21,bind([[_19070, _19147], [32 ^ [], identity_relation(32 ^ [])]]))).
% 29.52/29.37 cnf('1.2.1.2.1.1.1.1',plain,[-(relation(identity_relation(32 ^ [])))],extension(24,bind([[_22320], [32 ^ []]]))).
% 29.52/29.37 cnf('1.2.1.2.1.1.2',plain,[-(identity_relation(32 ^ []) = identity_relation(32 ^ [])), 32 ^ [] = 32 ^ []],extension(17,bind([[_15555, _15604], [32 ^ [], 32 ^ []]]))).
% 29.52/29.37 cnf('1.2.1.2.1.1.2.1',plain,[-(32 ^ [] = 32 ^ [])],extension(18,bind([[_12691], [32 ^ []]]))).
% 29.52/29.37 cnf('1.2.1.2.1.2',plain,[-(in(17 ^ [32 ^ [], identity_relation(32 ^ [])], 32 ^ [])), -(18 ^ [32 ^ [], identity_relation(32 ^ [])])],extension(4,bind([[_20601, _20492], [32 ^ [], identity_relation(32 ^ [])]]))).
% 29.52/29.37 cnf('1.2.1.2.1.2.1',plain,[18 ^ [32 ^ [], identity_relation(32 ^ [])]],reduction('1.2.1')).
% 29.52/29.37 cnf('1.2.1.2.1.3',plain,[-(17 ^ [32 ^ [], identity_relation(32 ^ [])] = 17 ^ [32 ^ [], identity_relation(32 ^ [])])],extension(18,bind([[_12691], [17 ^ [32 ^ [], identity_relation(32 ^ [])]]]))).
% 29.52/29.37 cnf('1.2.1.3',plain,[-(20 ^ [32 ^ [], identity_relation(32 ^ [])]), -(in(ordered_pair(19 ^ [32 ^ [], identity_relation(32 ^ [])], 17 ^ [32 ^ [], identity_relation(32 ^ [])]), identity_relation(32 ^ [])))],extension(2,bind([[_20601, _20492], [32 ^ [], identity_relation(32 ^ [])]]))).
% 29.52/29.37 cnf('1.2.1.3.1',plain,[in(ordered_pair(19 ^ [32 ^ [], identity_relation(32 ^ [])], 17 ^ [32 ^ [], identity_relation(32 ^ [])]), identity_relation(32 ^ [])), -(2 ^ [identity_relation(32 ^ []), 32 ^ []]), 1 ^ [17 ^ [32 ^ [], identity_relation(32 ^ [])], 19 ^ [32 ^ [], identity_relation(32 ^ [])], identity_relation(32 ^ []), 32 ^ []]],extension(14,bind([[_19398, _19336, _19147, _19070], [17 ^ [32 ^ [], identity_relation(32 ^ [])], 19 ^ [32 ^ [], identity_relation(32 ^ [])], identity_relation(32 ^ []), 32 ^ []]]))).
% 29.52/29.37 cnf('1.2.1.3.1.1',plain,[2 ^ [identity_relation(32 ^ []), 32 ^ []], -(7 ^ [identity_relation(32 ^ []), 32 ^ []]), identity_relation(32 ^ []) = identity_relation(32 ^ [])],extension(15,bind([[_19147, _19070], [identity_relation(32 ^ []), 32 ^ []]]))).
% 29.52/29.37 cnf('1.2.1.3.1.1.1',plain,[7 ^ [identity_relation(32 ^ []), 32 ^ []], relation(identity_relation(32 ^ []))],extension(21,bind([[_19070, _19147], [32 ^ [], identity_relation(32 ^ [])]]))).
% 29.52/29.37 cnf('1.2.1.3.1.1.1.1',plain,[-(relation(identity_relation(32 ^ [])))],extension(24,bind([[_22320], [32 ^ []]]))).
% 29.52/29.37 cnf('1.2.1.3.1.1.2',plain,[-(identity_relation(32 ^ []) = identity_relation(32 ^ [])), 32 ^ [] = 32 ^ []],extension(17,bind([[_15555, _15604], [32 ^ [], 32 ^ []]]))).
% 29.52/29.37 cnf('1.2.1.3.1.1.2.1',plain,[-(32 ^ [] = 32 ^ [])],extension(18,bind([[_12691], [32 ^ []]]))).
% 29.52/29.37 cnf('1.2.1.3.1.2',plain,[-(1 ^ [17 ^ [32 ^ [], identity_relation(32 ^ [])], 19 ^ [32 ^ [], identity_relation(32 ^ [])], identity_relation(32 ^ []), 32 ^ []]), -(19 ^ [32 ^ [], identity_relation(32 ^ [])] = 17 ^ [32 ^ [], identity_relation(32 ^ [])])],extension(11,bind([[_19147, _19070, _19336, _19398], [identity_relation(32 ^ []), 32 ^ [], 19 ^ [32 ^ [], identity_relation(32 ^ [])], 17 ^ [32 ^ [], identity_relation(32 ^ [])]]]))).
% 29.52/29.37 cnf('1.2.1.3.1.2.1',plain,[19 ^ [32 ^ [], identity_relation(32 ^ [])] = 17 ^ [32 ^ [], identity_relation(32 ^ [])], -(in(17 ^ [32 ^ [], identity_relation(32 ^ [])], 32 ^ [])), in(19 ^ [32 ^ [], identity_relation(32 ^ [])], 32 ^ []), 32 ^ [] = 32 ^ []],extension(20,bind([[_14619, _14552, _14685, _14750], [17 ^ [32 ^ [], identity_relation(32 ^ [])], 19 ^ [32 ^ [], identity_relation(32 ^ [])], 32 ^ [], 32 ^ []]]))).
% 29.52/29.37 cnf('1.2.1.3.1.2.1.1',plain,[in(17 ^ [32 ^ [], identity_relation(32 ^ [])], 32 ^ []), -(20 ^ [32 ^ [], identity_relation(32 ^ [])])],extension(1,bind([[_20601, _20492], [32 ^ [], identity_relation(32 ^ [])]]))).
% 29.52/29.37 cnf('1.2.1.3.1.2.1.1.1',plain,[20 ^ [32 ^ [], identity_relation(32 ^ [])]],reduction('1.2.1')).
% 29.52/29.37 cnf('1.2.1.3.1.2.1.2',plain,[-(in(19 ^ [32 ^ [], identity_relation(32 ^ [])], 32 ^ [])), -(1 ^ [17 ^ [32 ^ [], identity_relation(32 ^ [])], 19 ^ [32 ^ [], identity_relation(32 ^ [])], identity_relation(32 ^ []), 32 ^ []])],extension(12,bind([[_19398, _19336, _19147, _19070], [17 ^ [32 ^ [], identity_relation(32 ^ [])], 19 ^ [32 ^ [], identity_relation(32 ^ [])], identity_relation(32 ^ []), 32 ^ []]]))).
% 29.52/29.37 cnf('1.2.1.3.1.2.1.2.1',plain,[1 ^ [17 ^ [32 ^ [], identity_relation(32 ^ [])], 19 ^ [32 ^ [], identity_relation(32 ^ [])], identity_relation(32 ^ []), 32 ^ []]],reduction('1.2.1.3.1')).
% 29.52/29.37 cnf('1.2.1.3.1.2.1.3',plain,[-(32 ^ [] = 32 ^ [])],extension(18,bind([[_12691], [32 ^ []]]))).
% 29.52/29.37 %-----------------------------------------------------
% 29.55/29.38
% 29.55/29.38 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------