%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU058+1 : TPTP v8.1.0. Bugfixed v4.0.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 11:59:59 EDT 2022
% Result : Theorem 1.81s 2.44s
% Output : Proof 1.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU058+1 : TPTP v8.1.0. Bugfixed v4.0.0.
% 0.03/0.13 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n005.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Sun Jun 19 01:14:53 EDT 2022
% 0.12/0.34 % CPUTime :
% 1.81/2.44 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.81/2.45 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.81/2.46
% 1.81/2.46 %-----------------------------------------------------
% 1.81/2.46 fof(t137_funct_1, conjecture, ! [_81043, _81046, _81049] : (relation(_81049) & function(_81049) => relation_inverse_image(_81049, set_intersection2(_81043, _81046)) = set_intersection2(relation_inverse_image(_81049, _81043), relation_inverse_image(_81049, _81046))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t137_funct_1)).
% 1.81/2.46 fof(d13_funct_1, axiom, ! [_81388] : (relation(_81388) & function(_81388) => ! [_81410, _81413] : (_81413 = relation_inverse_image(_81388, _81410) <=> ! [_81434] : (in(_81434, _81413) <=> in(_81434, relation_dom(_81388)) & in(apply(_81388, _81434), _81410)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d13_funct_1)).
% 1.81/2.46 fof(d3_xboole_0, axiom, ! [_81756, _81759, _81762] : (_81762 = set_intersection2(_81756, _81759) <=> ! [_81783] : (in(_81783, _81762) <=> in(_81783, _81756) & in(_81783, _81759))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d3_xboole_0)).
% 1.81/2.46
% 1.81/2.46 cnf(1, plain, [-(relation(17 ^ []))], clausify(t137_funct_1)).
% 1.81/2.46 cnf(2, plain, [-(function(17 ^ []))], clausify(t137_funct_1)).
% 1.81/2.46 cnf(3, plain, [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = set_intersection2(relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], 16 ^ []))], clausify(t137_funct_1)).
% 1.81/2.46 cnf(4, plain, [_20755 = _20804, -(relation_dom(_20755) = relation_dom(_20804))], theory(equality)).
% 1.81/2.46 cnf(5, plain, [-(relation_inverse_image(_21084, _21217) = relation_inverse_image(_21151, _21282)), _21084 = _21151, _21217 = _21282], theory(equality)).
% 1.81/2.46 cnf(6, plain, [-(set_intersection2(_21698, _21831) = set_intersection2(_21765, _21896)), _21698 = _21765, _21831 = _21896], theory(equality)).
% 1.81/2.46 cnf(7, plain, [-(_15267 = _15267)], theory(equality)).
% 1.81/2.46 cnf(8, plain, [-(in(_17524, _17655)), in(_17457, _17590), _17457 = _17524, _17590 = _17655], theory(equality)).
% 1.81/2.46 cnf(9, plain, [function(_23920), relation(_23920), _24170 = relation_inverse_image(_23920, _24096), in(_24339, _24170), -(in(_24339, relation_dom(_23920)))], clausify(d13_funct_1)).
% 1.81/2.46 cnf(10, plain, [function(_23920), relation(_23920), _24170 = relation_inverse_image(_23920, _24096), in(_24339, _24170), -(in(apply(_23920, _24339), _24096))], clausify(d13_funct_1)).
% 1.81/2.46 cnf(11, plain, [function(_23920), relation(_23920), _24170 = relation_inverse_image(_23920, _24096), -(in(_24339, _24170)), in(_24339, relation_dom(_23920)), in(apply(_23920, _24339), _24096)], clausify(d13_funct_1)).
% 1.81/2.46 cnf(12, plain, [_24933 = set_intersection2(_24794, _24864), in(_25097, _24933), -(in(_25097, _24794))], clausify(d3_xboole_0)).
% 1.81/2.46 cnf(13, plain, [_24933 = set_intersection2(_24794, _24864), in(_25097, _24933), -(in(_25097, _24864))], clausify(d3_xboole_0)).
% 1.81/2.46 cnf(14, plain, [_24933 = set_intersection2(_24794, _24864), -(in(_25097, _24933)), in(_25097, _24794), in(_25097, _24864)], clausify(d3_xboole_0)).
% 1.81/2.46 cnf(15, plain, [-(_24933 = set_intersection2(_24794, _24864)), -(in(2 ^ [_24933, _24864, _24794], _24933)), -(in(2 ^ [_24933, _24864, _24794], _24794))], clausify(d3_xboole_0)).
% 1.81/2.46 cnf(16, plain, [-(_24933 = set_intersection2(_24794, _24864)), -(in(2 ^ [_24933, _24864, _24794], _24933)), -(in(2 ^ [_24933, _24864, _24794], _24864))], clausify(d3_xboole_0)).
% 1.81/2.46 cnf(17, plain, [-(_24933 = set_intersection2(_24794, _24864)), in(2 ^ [_24933, _24864, _24794], _24933), in(2 ^ [_24933, _24864, _24794], _24794), in(2 ^ [_24933, _24864, _24794], _24864)], clausify(d3_xboole_0)).
% 1.81/2.46
% 1.81/2.46 cnf('1',plain,[relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = set_intersection2(relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], 16 ^ []))],start(3)).
% 1.81/2.46 cnf('1.1',plain,[-(relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = set_intersection2(relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], 16 ^ []))), in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ []))), in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], 15 ^ [])), in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], 16 ^ []))],extension(17,bind([[_24933, _24794, _24864], [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], 16 ^ [])]]))).
% 1.81/2.46 cnf('1.1.1',plain,[-(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])))), function(17 ^ []), relation(17 ^ []), relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_dom(17 ^ [])), in(apply(17 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])]), set_intersection2(15 ^ [], 16 ^ []))],extension(11,bind([[_24170, _23920, _24339, _24096], [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), 17 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], set_intersection2(15 ^ [], 16 ^ [])]]))).
% 1.81/2.46 cnf('1.1.1.1',plain,[-(function(17 ^ []))],extension(2)).
% 1.81/2.46 cnf('1.1.1.2',plain,[-(relation(17 ^ []))],extension(1)).
% 1.81/2.46 cnf('1.1.1.3',plain,[-(relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ []))), 17 ^ [] = 17 ^ [], set_intersection2(15 ^ [], 16 ^ []) = set_intersection2(15 ^ [], 16 ^ [])],extension(5,bind([[_21084, _21151, _21217, _21282], [17 ^ [], 17 ^ [], set_intersection2(15 ^ [], 16 ^ []), set_intersection2(15 ^ [], 16 ^ [])]]))).
% 1.81/2.46 cnf('1.1.1.3.1',plain,[-(17 ^ [] = 17 ^ [])],extension(7,bind([[_15267], [17 ^ []]]))).
% 1.81/2.46 cnf('1.1.1.3.2',plain,[-(set_intersection2(15 ^ [], 16 ^ []) = set_intersection2(15 ^ [], 16 ^ [])), 15 ^ [] = 15 ^ [], 16 ^ [] = 16 ^ []],extension(6,bind([[_21698, _21765, _21831, _21896], [15 ^ [], 15 ^ [], 16 ^ [], 16 ^ []]]))).
% 1.81/2.46 cnf('1.1.1.3.2.1',plain,[-(15 ^ [] = 15 ^ [])],extension(7,bind([[_15267], [15 ^ []]]))).
% 1.81/2.46 cnf('1.1.1.3.2.2',plain,[-(16 ^ [] = 16 ^ [])],extension(7,bind([[_15267], [16 ^ []]]))).
% 1.81/2.46 cnf('1.1.1.4',plain,[-(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_dom(17 ^ []))), in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_dom(17 ^ [])), 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])] = 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_dom(17 ^ []) = relation_dom(17 ^ [])],extension(8,bind([[_17457, _17524, _17590, _17655], [2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_dom(17 ^ []), relation_dom(17 ^ [])]]))).
% 1.81/2.46 cnf('1.1.1.4.1',plain,[-(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_dom(17 ^ []))), function(17 ^ []), relation(17 ^ []), relation_inverse_image(17 ^ [], 15 ^ []) = relation_inverse_image(17 ^ [], 15 ^ []), in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], 15 ^ []))],extension(9,bind([[_23920, _24096, _24339, _24170], [17 ^ [], 15 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], 15 ^ [])]]))).
% 1.81/2.46 cnf('1.1.1.4.1.1',plain,[-(function(17 ^ []))],extension(2)).
% 1.81/2.46 cnf('1.1.1.4.1.2',plain,[-(relation(17 ^ []))],extension(1)).
% 1.81/2.46 cnf('1.1.1.4.1.3',plain,[-(relation_inverse_image(17 ^ [], 15 ^ []) = relation_inverse_image(17 ^ [], 15 ^ []))],extension(7,bind([[_15267], [relation_inverse_image(17 ^ [], 15 ^ [])]]))).
% 1.81/2.46 cnf('1.1.1.4.1.4',plain,[-(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], 15 ^ []))), -(relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = set_intersection2(relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], 16 ^ []))), -(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ []))))],extension(15,bind([[_24864, _24794, _24933], [relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ []))]]))).
% 1.81/2.46 cnf('1.1.1.4.1.4.1',plain,[relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = set_intersection2(relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], 16 ^ []))],extension(3)).
% 1.81/2.46 cnf('1.1.1.4.1.4.2',plain,[in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])))],reduction('1.1')).
% 1.81/2.46 cnf('1.1.1.4.2',plain,[-(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])] = 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])])],extension(7,bind([[_15267], [2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])]]]))).
% 1.81/2.46 cnf('1.1.1.4.3',plain,[-(relation_dom(17 ^ []) = relation_dom(17 ^ [])), 17 ^ [] = 17 ^ []],extension(4,bind([[_20755, _20804], [17 ^ [], 17 ^ []]]))).
% 1.81/2.46 cnf('1.1.1.4.3.1',plain,[-(17 ^ [] = 17 ^ [])],extension(7,bind([[_15267], [17 ^ []]]))).
% 1.81/2.46 cnf('1.1.1.5',plain,[-(in(apply(17 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])]), set_intersection2(15 ^ [], 16 ^ []))), set_intersection2(15 ^ [], 16 ^ []) = set_intersection2(15 ^ [], 16 ^ []), in(apply(17 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])]), 15 ^ []), in(apply(17 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])]), 16 ^ [])],extension(14,bind([[_24933, _24794, _25097, _24864], [set_intersection2(15 ^ [], 16 ^ []), 15 ^ [], apply(17 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])]), 16 ^ []]]))).
% 1.81/2.46 cnf('1.1.1.5.1',plain,[-(set_intersection2(15 ^ [], 16 ^ []) = set_intersection2(15 ^ [], 16 ^ [])), 15 ^ [] = 15 ^ [], 16 ^ [] = 16 ^ []],extension(6,bind([[_21698, _21765, _21831, _21896], [15 ^ [], 15 ^ [], 16 ^ [], 16 ^ []]]))).
% 1.81/2.46 cnf('1.1.1.5.1.1',plain,[-(15 ^ [] = 15 ^ [])],extension(7,bind([[_15267], [15 ^ []]]))).
% 1.81/2.46 cnf('1.1.1.5.1.2',plain,[-(16 ^ [] = 16 ^ [])],extension(7,bind([[_15267], [16 ^ []]]))).
% 1.81/2.46 cnf('1.1.1.5.2',plain,[-(in(apply(17 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])]), 15 ^ [])), function(17 ^ []), relation(17 ^ []), relation_inverse_image(17 ^ [], 15 ^ []) = relation_inverse_image(17 ^ [], 15 ^ []), in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], 15 ^ []))],extension(10,bind([[_23920, _24096, _24339, _24170], [17 ^ [], 15 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], 15 ^ [])]]))).
% 1.81/2.46 cnf('1.1.1.5.2.1',plain,[-(function(17 ^ []))],extension(2)).
% 1.81/2.46 cnf('1.1.1.5.2.2',plain,[-(relation(17 ^ []))],extension(1)).
% 1.81/2.46 cnf('1.1.1.5.2.3',plain,[-(relation_inverse_image(17 ^ [], 15 ^ []) = relation_inverse_image(17 ^ [], 15 ^ []))],extension(7,bind([[_15267], [relation_inverse_image(17 ^ [], 15 ^ [])]]))).
% 1.81/2.46 cnf('1.1.1.5.2.4',plain,[-(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], 15 ^ []))), -(relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = set_intersection2(relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], 16 ^ []))), -(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ []))))],extension(15,bind([[_24864, _24794, _24933], [relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ []))]]))).
% 1.81/2.46 cnf('1.1.1.5.2.4.1',plain,[relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = set_intersection2(relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], 16 ^ []))],extension(3)).
% 1.81/2.46 cnf('1.1.1.5.2.4.2',plain,[in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])))],reduction('1.1')).
% 1.81/2.46 cnf('1.1.1.5.3',plain,[-(in(apply(17 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])]), 16 ^ [])), function(17 ^ []), relation(17 ^ []), relation_inverse_image(17 ^ [], 16 ^ []) = relation_inverse_image(17 ^ [], 16 ^ []), in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], 16 ^ []))],extension(10,bind([[_23920, _24096, _24339, _24170], [17 ^ [], 16 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], 16 ^ [])]]))).
% 1.81/2.46 cnf('1.1.1.5.3.1',plain,[-(function(17 ^ []))],extension(2)).
% 1.81/2.46 cnf('1.1.1.5.3.2',plain,[-(relation(17 ^ []))],extension(1)).
% 1.81/2.46 cnf('1.1.1.5.3.3',plain,[-(relation_inverse_image(17 ^ [], 16 ^ []) = relation_inverse_image(17 ^ [], 16 ^ []))],extension(7,bind([[_15267], [relation_inverse_image(17 ^ [], 16 ^ [])]]))).
% 1.81/2.46 cnf('1.1.1.5.3.4',plain,[-(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], 16 ^ []))), -(relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = set_intersection2(relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], 16 ^ []))), -(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ []))))],extension(16,bind([[_24864, _24794, _24933], [relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ []))]]))).
% 1.81/2.46 cnf('1.1.1.5.3.4.1',plain,[relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = set_intersection2(relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], 16 ^ []))],extension(3)).
% 1.81/2.46 cnf('1.1.1.5.3.4.2',plain,[in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])))],reduction('1.1')).
% 1.81/2.46 cnf('1.1.2',plain,[-(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], 15 ^ []))), function(17 ^ []), relation(17 ^ []), relation_inverse_image(17 ^ [], 15 ^ []) = relation_inverse_image(17 ^ [], 15 ^ []), in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_dom(17 ^ [])), in(apply(17 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])]), 15 ^ [])],extension(11,bind([[_24170, _23920, _24339, _24096], [relation_inverse_image(17 ^ [], 15 ^ []), 17 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], 15 ^ []]]))).
% 1.81/2.46 cnf('1.1.2.1',plain,[-(function(17 ^ []))],extension(2)).
% 1.81/2.46 cnf('1.1.2.2',plain,[-(relation(17 ^ []))],extension(1)).
% 1.81/2.46 cnf('1.1.2.3',plain,[-(relation_inverse_image(17 ^ [], 15 ^ []) = relation_inverse_image(17 ^ [], 15 ^ [])), 17 ^ [] = 17 ^ [], 15 ^ [] = 15 ^ []],extension(5,bind([[_21084, _21151, _21217, _21282], [17 ^ [], 17 ^ [], 15 ^ [], 15 ^ []]]))).
% 1.81/2.46 cnf('1.1.2.3.1',plain,[-(17 ^ [] = 17 ^ [])],extension(7,bind([[_15267], [17 ^ []]]))).
% 1.81/2.46 cnf('1.1.2.3.2',plain,[-(15 ^ [] = 15 ^ [])],extension(7,bind([[_15267], [15 ^ []]]))).
% 1.81/2.46 cnf('1.1.2.4',plain,[-(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_dom(17 ^ []))), in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_dom(17 ^ [])), 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])] = 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_dom(17 ^ []) = relation_dom(17 ^ [])],extension(8,bind([[_17457, _17524, _17590, _17655], [2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_dom(17 ^ []), relation_dom(17 ^ [])]]))).
% 1.81/2.46 cnf('1.1.2.4.1',plain,[-(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_dom(17 ^ []))), function(17 ^ []), relation(17 ^ []), relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])))],extension(9,bind([[_23920, _24096, _24339, _24170], [17 ^ [], set_intersection2(15 ^ [], 16 ^ []), 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ []))]]))).
% 1.81/2.46 cnf('1.1.2.4.1.1',plain,[-(function(17 ^ []))],extension(2)).
% 1.81/2.46 cnf('1.1.2.4.1.2',plain,[-(relation(17 ^ []))],extension(1)).
% 1.81/2.46 cnf('1.1.2.4.1.3',plain,[-(relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])))],extension(7,bind([[_15267], [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ []))]]))).
% 1.81/2.46 cnf('1.1.2.4.1.4',plain,[-(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])))), -(relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = set_intersection2(relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], 16 ^ []))), -(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], 15 ^ [])))],extension(15,bind([[_24933, _24864, _24794], [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])]]))).
% 1.81/2.46 cnf('1.1.2.4.1.4.1',plain,[relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = set_intersection2(relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], 16 ^ []))],extension(3)).
% 1.81/2.46 cnf('1.1.2.4.1.4.2',plain,[in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], 15 ^ []))],reduction('1.1')).
% 1.81/2.46 cnf('1.1.2.4.2',plain,[-(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])] = 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])])],extension(7,bind([[_15267], [2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])]]]))).
% 1.81/2.46 cnf('1.1.2.4.3',plain,[-(relation_dom(17 ^ []) = relation_dom(17 ^ [])), 17 ^ [] = 17 ^ []],extension(4,bind([[_20755, _20804], [17 ^ [], 17 ^ []]]))).
% 1.81/2.46 cnf('1.1.2.4.3.1',plain,[-(17 ^ [] = 17 ^ [])],extension(7,bind([[_15267], [17 ^ []]]))).
% 1.81/2.46 cnf('1.1.2.5',plain,[-(in(apply(17 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])]), 15 ^ [])), set_intersection2(15 ^ [], 16 ^ []) = set_intersection2(15 ^ [], 16 ^ []), in(apply(17 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])]), set_intersection2(15 ^ [], 16 ^ []))],extension(12,bind([[_24794, _24864, _25097, _24933], [15 ^ [], 16 ^ [], apply(17 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])]), set_intersection2(15 ^ [], 16 ^ [])]]))).
% 1.81/2.46 cnf('1.1.2.5.1',plain,[-(set_intersection2(15 ^ [], 16 ^ []) = set_intersection2(15 ^ [], 16 ^ [])), 15 ^ [] = 15 ^ [], 16 ^ [] = 16 ^ []],extension(6,bind([[_21698, _21765, _21831, _21896], [15 ^ [], 15 ^ [], 16 ^ [], 16 ^ []]]))).
% 1.81/2.46 cnf('1.1.2.5.1.1',plain,[-(15 ^ [] = 15 ^ [])],extension(7,bind([[_15267], [15 ^ []]]))).
% 1.81/2.46 cnf('1.1.2.5.1.2',plain,[-(16 ^ [] = 16 ^ [])],extension(7,bind([[_15267], [16 ^ []]]))).
% 1.81/2.46 cnf('1.1.2.5.2',plain,[-(in(apply(17 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])]), set_intersection2(15 ^ [], 16 ^ []))), function(17 ^ []), relation(17 ^ []), relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])))],extension(10,bind([[_23920, _24096, _24339, _24170], [17 ^ [], set_intersection2(15 ^ [], 16 ^ []), 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ []))]]))).
% 1.81/2.46 cnf('1.1.2.5.2.1',plain,[-(function(17 ^ []))],extension(2)).
% 1.81/2.46 cnf('1.1.2.5.2.2',plain,[-(relation(17 ^ []))],extension(1)).
% 1.81/2.46 cnf('1.1.2.5.2.3',plain,[-(relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])))],extension(7,bind([[_15267], [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ []))]]))).
% 1.81/2.46 cnf('1.1.2.5.2.4',plain,[-(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])))), -(relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = set_intersection2(relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], 16 ^ []))), -(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], 15 ^ [])))],extension(15,bind([[_24933, _24864, _24794], [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])]]))).
% 1.81/2.46 cnf('1.1.2.5.2.4.1',plain,[relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = set_intersection2(relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], 16 ^ []))],extension(3)).
% 1.81/2.46 cnf('1.1.2.5.2.4.2',plain,[in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], 15 ^ []))],reduction('1.1')).
% 1.81/2.46 cnf('1.1.3',plain,[-(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], 16 ^ []))), function(17 ^ []), relation(17 ^ []), relation_inverse_image(17 ^ [], 16 ^ []) = relation_inverse_image(17 ^ [], 16 ^ []), in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_dom(17 ^ [])), in(apply(17 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])]), 16 ^ [])],extension(11,bind([[_24170, _23920, _24339, _24096], [relation_inverse_image(17 ^ [], 16 ^ []), 17 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], 16 ^ []]]))).
% 1.81/2.46 cnf('1.1.3.1',plain,[-(function(17 ^ []))],extension(2)).
% 1.81/2.46 cnf('1.1.3.2',plain,[-(relation(17 ^ []))],extension(1)).
% 1.81/2.46 cnf('1.1.3.3',plain,[-(relation_inverse_image(17 ^ [], 16 ^ []) = relation_inverse_image(17 ^ [], 16 ^ [])), 17 ^ [] = 17 ^ [], 16 ^ [] = 16 ^ []],extension(5,bind([[_21084, _21151, _21217, _21282], [17 ^ [], 17 ^ [], 16 ^ [], 16 ^ []]]))).
% 1.81/2.46 cnf('1.1.3.3.1',plain,[-(17 ^ [] = 17 ^ [])],extension(7,bind([[_15267], [17 ^ []]]))).
% 1.81/2.46 cnf('1.1.3.3.2',plain,[-(16 ^ [] = 16 ^ [])],extension(7,bind([[_15267], [16 ^ []]]))).
% 1.81/2.46 cnf('1.1.3.4',plain,[-(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_dom(17 ^ []))), in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_dom(17 ^ [])), 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])] = 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_dom(17 ^ []) = relation_dom(17 ^ [])],extension(8,bind([[_17457, _17524, _17590, _17655], [2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_dom(17 ^ []), relation_dom(17 ^ [])]]))).
% 1.81/2.46 cnf('1.1.3.4.1',plain,[-(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_dom(17 ^ []))), function(17 ^ []), relation(17 ^ []), relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])))],extension(9,bind([[_23920, _24096, _24339, _24170], [17 ^ [], set_intersection2(15 ^ [], 16 ^ []), 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ []))]]))).
% 1.81/2.46 cnf('1.1.3.4.1.1',plain,[-(function(17 ^ []))],extension(2)).
% 1.81/2.46 cnf('1.1.3.4.1.2',plain,[-(relation(17 ^ []))],extension(1)).
% 1.81/2.46 cnf('1.1.3.4.1.3',plain,[-(relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])))],extension(7,bind([[_15267], [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ []))]]))).
% 1.81/2.46 cnf('1.1.3.4.1.4',plain,[-(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])))), -(relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = set_intersection2(relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], 16 ^ []))), -(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], 16 ^ [])))],extension(16,bind([[_24933, _24794, _24864], [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], 16 ^ [])]]))).
% 1.81/2.46 cnf('1.1.3.4.1.4.1',plain,[relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = set_intersection2(relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], 16 ^ []))],extension(3)).
% 1.81/2.46 cnf('1.1.3.4.1.4.2',plain,[in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], 16 ^ []))],reduction('1.1')).
% 1.81/2.46 cnf('1.1.3.4.2',plain,[-(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])] = 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])])],extension(7,bind([[_15267], [2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])]]]))).
% 1.81/2.46 cnf('1.1.3.4.3',plain,[-(relation_dom(17 ^ []) = relation_dom(17 ^ [])), 17 ^ [] = 17 ^ []],extension(4,bind([[_20755, _20804], [17 ^ [], 17 ^ []]]))).
% 1.81/2.46 cnf('1.1.3.4.3.1',plain,[-(17 ^ [] = 17 ^ [])],extension(7,bind([[_15267], [17 ^ []]]))).
% 1.81/2.46 cnf('1.1.3.5',plain,[-(in(apply(17 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])]), 16 ^ [])), set_intersection2(15 ^ [], 16 ^ []) = set_intersection2(15 ^ [], 16 ^ []), in(apply(17 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])]), set_intersection2(15 ^ [], 16 ^ []))],extension(13,bind([[_24794, _24864, _25097, _24933], [15 ^ [], 16 ^ [], apply(17 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])]), set_intersection2(15 ^ [], 16 ^ [])]]))).
% 1.81/2.46 cnf('1.1.3.5.1',plain,[-(set_intersection2(15 ^ [], 16 ^ []) = set_intersection2(15 ^ [], 16 ^ [])), 15 ^ [] = 15 ^ [], 16 ^ [] = 16 ^ []],extension(6,bind([[_21698, _21765, _21831, _21896], [15 ^ [], 15 ^ [], 16 ^ [], 16 ^ []]]))).
% 1.81/2.46 cnf('1.1.3.5.1.1',plain,[-(15 ^ [] = 15 ^ [])],extension(7,bind([[_15267], [15 ^ []]]))).
% 1.81/2.46 cnf('1.1.3.5.1.2',plain,[-(16 ^ [] = 16 ^ [])],extension(7,bind([[_15267], [16 ^ []]]))).
% 1.81/2.46 cnf('1.1.3.5.2',plain,[-(in(apply(17 ^ [], 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])]), set_intersection2(15 ^ [], 16 ^ []))), function(17 ^ []), relation(17 ^ []), relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])))],extension(10,bind([[_23920, _24096, _24339, _24170], [17 ^ [], set_intersection2(15 ^ [], 16 ^ []), 2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ []))]]))).
% 1.81/2.46 cnf('1.1.3.5.2.1',plain,[-(function(17 ^ []))],extension(2)).
% 1.81/2.46 cnf('1.1.3.5.2.2',plain,[-(relation(17 ^ []))],extension(1)).
% 1.81/2.46 cnf('1.1.3.5.2.3',plain,[-(relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])))],extension(7,bind([[_15267], [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ []))]]))).
% 1.81/2.46 cnf('1.1.3.5.2.4',plain,[-(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])))), -(relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = set_intersection2(relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], 16 ^ []))), -(in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], 16 ^ [])))],extension(16,bind([[_24933, _24794, _24864], [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], 16 ^ [])]]))).
% 1.81/2.46 cnf('1.1.3.5.2.4.1',plain,[relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])) = set_intersection2(relation_inverse_image(17 ^ [], 15 ^ []), relation_inverse_image(17 ^ [], 16 ^ []))],extension(3)).
% 1.81/2.46 cnf('1.1.3.5.2.4.2',plain,[in(2 ^ [relation_inverse_image(17 ^ [], set_intersection2(15 ^ [], 16 ^ [])), relation_inverse_image(17 ^ [], 16 ^ []), relation_inverse_image(17 ^ [], 15 ^ [])], relation_inverse_image(17 ^ [], 16 ^ []))],reduction('1.1')).
% 1.81/2.46 %-----------------------------------------------------
% 1.81/2.46
% 1.81/2.46 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------