%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU166+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n016.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:40 EDT 2022
% Result : Theorem 1.00s 1.45s
% Output : Proof 1.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SEU166+1 : TPTP v8.1.0. Released v3.3.0.
% 0.08/0.15 % Command : leancop_casc.sh %s %d
% 0.15/0.36 % Computer : n016.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 600
% 0.15/0.36 % DateTime : Sun Jun 19 06:23:38 EDT 2022
% 0.15/0.36 % CPUTime :
% 1.00/1.45 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.00/1.46 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.10/1.47
% 1.10/1.47 %-----------------------------------------------------
% 1.10/1.47 fof(t118_zfmisc_1, conjecture, ! [_45024, _45027, _45030] : (subset(_45024, _45027) => subset(cartesian_product2(_45024, _45030), cartesian_product2(_45027, _45030)) & subset(cartesian_product2(_45030, _45024), cartesian_product2(_45030, _45027))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t118_zfmisc_1)).
% 1.10/1.47 fof(d2_zfmisc_1, axiom, ! [_45329, _45332, _45335] : (_45335 = cartesian_product2(_45329, _45332) <=> ! [_45356] : (in(_45356, _45335) <=> ? [_45374, _45377] : (in(_45374, _45329) & in(_45377, _45332) & _45356 = ordered_pair(_45374, _45377)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d2_zfmisc_1)).
% 1.10/1.47 fof(d3_tarski, axiom, ! [_45705, _45708] : (subset(_45705, _45708) <=> ! [_45726] : (in(_45726, _45705) => in(_45726, _45708))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d3_tarski)).
% 1.10/1.47
% 1.10/1.47 cnf(1, plain, [-(subset(9 ^ [], 10 ^ []))], clausify(t118_zfmisc_1)).
% 1.10/1.47 cnf(2, plain, [subset(cartesian_product2(9 ^ [], 11 ^ []), cartesian_product2(10 ^ [], 11 ^ [])), subset(cartesian_product2(11 ^ [], 9 ^ []), cartesian_product2(11 ^ [], 10 ^ []))], clausify(t118_zfmisc_1)).
% 1.10/1.47 cnf(3, plain, [-(cartesian_product2(_9236, _9369) = cartesian_product2(_9303, _9434)), _9236 = _9303, _9369 = _9434], theory(equality)).
% 1.10/1.47 cnf(4, plain, [-(_6716 = _6716)], theory(equality)).
% 1.10/1.47 cnf(5, plain, [-(in(_8020, _8151)), in(_7953, _8086), _7953 = _8020, _8086 = _8151], theory(equality)).
% 1.10/1.47 cnf(6, plain, [_12325 = cartesian_product2(_12148, _12237), in(_12508, _12325), -(in(1 ^ [_12508, _12325, _12237, _12148], _12148))], clausify(d2_zfmisc_1)).
% 1.10/1.47 cnf(7, plain, [_12325 = cartesian_product2(_12148, _12237), in(_12508, _12325), -(in(2 ^ [_12508, _12325, _12237, _12148], _12237))], clausify(d2_zfmisc_1)).
% 1.10/1.47 cnf(8, plain, [_12325 = cartesian_product2(_12148, _12237), in(_12508, _12325), -(_12508 = ordered_pair(1 ^ [_12508, _12325, _12237, _12148], 2 ^ [_12508, _12325, _12237, _12148]))], clausify(d2_zfmisc_1)).
% 1.10/1.47 cnf(9, plain, [_12325 = cartesian_product2(_12148, _12237), -(in(_12508, _12325)), in(_12645, _12148), in(_12716, _12237), _12508 = ordered_pair(_12645, _12716)], clausify(d2_zfmisc_1)).
% 1.10/1.47 cnf(10, plain, [-(subset(_13175, _13231)), -(in(6 ^ [_13231, _13175], _13175))], clausify(d3_tarski)).
% 1.10/1.47 cnf(11, plain, [-(subset(_13175, _13231)), in(6 ^ [_13231, _13175], _13231)], clausify(d3_tarski)).
% 1.10/1.47 cnf(12, plain, [subset(_13175, _13231), in(_13345, _13175), -(in(_13345, _13231))], clausify(d3_tarski)).
% 1.10/1.47
% 1.10/1.47 cnf('1',plain,[subset(cartesian_product2(9 ^ [], 11 ^ []), cartesian_product2(10 ^ [], 11 ^ [])), subset(cartesian_product2(11 ^ [], 9 ^ []), cartesian_product2(11 ^ [], 10 ^ []))],start(2)).
% 1.10/1.47 cnf('1.1',plain,[-(subset(cartesian_product2(9 ^ [], 11 ^ []), cartesian_product2(10 ^ [], 11 ^ []))), in(6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(10 ^ [], 11 ^ []))],extension(11,bind([[_13175, _13231], [cartesian_product2(9 ^ [], 11 ^ []), cartesian_product2(10 ^ [], 11 ^ [])]]))).
% 1.10/1.47 cnf('1.1.1',plain,[-(in(6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(10 ^ [], 11 ^ []))), cartesian_product2(10 ^ [], 11 ^ []) = cartesian_product2(10 ^ [], 11 ^ []), in(1 ^ [6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []), 11 ^ [], 9 ^ []], 10 ^ []), in(2 ^ [6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []), 11 ^ [], 9 ^ []], 11 ^ []), 6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])] = ordered_pair(1 ^ [6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []), 11 ^ [], 9 ^ []], 2 ^ [6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []), 11 ^ [], 9 ^ []])],extension(9,bind([[_12325, _12148, _12237, _12508, _12645, _12716], [cartesian_product2(10 ^ [], 11 ^ []), 10 ^ [], 11 ^ [], 6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], 1 ^ [6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []), 11 ^ [], 9 ^ []], 2 ^ [6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []), 11 ^ [], 9 ^ []]]]))).
% 1.10/1.47 cnf('1.1.1.1',plain,[-(cartesian_product2(10 ^ [], 11 ^ []) = cartesian_product2(10 ^ [], 11 ^ [])), 10 ^ [] = 10 ^ [], 11 ^ [] = 11 ^ []],extension(3,bind([[_9236, _9303, _9369, _9434], [10 ^ [], 10 ^ [], 11 ^ [], 11 ^ []]]))).
% 1.10/1.47 cnf('1.1.1.1.1',plain,[-(10 ^ [] = 10 ^ [])],extension(4,bind([[_6716], [10 ^ []]]))).
% 1.10/1.47 cnf('1.1.1.1.2',plain,[-(11 ^ [] = 11 ^ [])],extension(4,bind([[_6716], [11 ^ []]]))).
% 1.10/1.47 cnf('1.1.1.2',plain,[-(in(1 ^ [6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []), 11 ^ [], 9 ^ []], 10 ^ [])), subset(9 ^ [], 10 ^ []), in(1 ^ [6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []), 11 ^ [], 9 ^ []], 9 ^ [])],extension(12,bind([[_13231, _13345, _13175], [10 ^ [], 1 ^ [6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []), 11 ^ [], 9 ^ []], 9 ^ []]]))).
% 1.10/1.47 cnf('1.1.1.2.1',plain,[-(subset(9 ^ [], 10 ^ []))],extension(1)).
% 1.10/1.47 cnf('1.1.1.2.2',plain,[-(in(1 ^ [6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []), 11 ^ [], 9 ^ []], 9 ^ [])), cartesian_product2(9 ^ [], 11 ^ []) = cartesian_product2(9 ^ [], 11 ^ []), in(6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []))],extension(6,bind([[_12148, _12237, _12508, _12325], [9 ^ [], 11 ^ [], 6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ [])]]))).
% 1.10/1.47 cnf('1.1.1.2.2.1',plain,[-(cartesian_product2(9 ^ [], 11 ^ []) = cartesian_product2(9 ^ [], 11 ^ []))],extension(4,bind([[_6716], [cartesian_product2(9 ^ [], 11 ^ [])]]))).
% 1.10/1.47 cnf('1.1.1.2.2.2',plain,[-(in(6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []))), -(subset(cartesian_product2(9 ^ [], 11 ^ []), cartesian_product2(10 ^ [], 11 ^ [])))],extension(10,bind([[_13175, _13231], [cartesian_product2(9 ^ [], 11 ^ []), cartesian_product2(10 ^ [], 11 ^ [])]]))).
% 1.10/1.47 cnf('1.1.1.2.2.2.1',plain,[subset(cartesian_product2(9 ^ [], 11 ^ []), cartesian_product2(10 ^ [], 11 ^ []))],reduction('1')).
% 1.10/1.47 cnf('1.1.1.3',plain,[-(in(2 ^ [6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []), 11 ^ [], 9 ^ []], 11 ^ [])), cartesian_product2(9 ^ [], 11 ^ []) = cartesian_product2(9 ^ [], 11 ^ []), in(6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []))],extension(7,bind([[_12148, _12237, _12508, _12325], [9 ^ [], 11 ^ [], 6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ [])]]))).
% 1.10/1.47 cnf('1.1.1.3.1',plain,[-(cartesian_product2(9 ^ [], 11 ^ []) = cartesian_product2(9 ^ [], 11 ^ [])), 9 ^ [] = 9 ^ [], 11 ^ [] = 11 ^ []],extension(3,bind([[_9236, _9303, _9369, _9434], [9 ^ [], 9 ^ [], 11 ^ [], 11 ^ []]]))).
% 1.10/1.47 cnf('1.1.1.3.1.1',plain,[-(9 ^ [] = 9 ^ [])],extension(4,bind([[_6716], [9 ^ []]]))).
% 1.10/1.47 cnf('1.1.1.3.1.2',plain,[-(11 ^ [] = 11 ^ [])],extension(4,bind([[_6716], [11 ^ []]]))).
% 1.10/1.47 cnf('1.1.1.3.2',plain,[-(in(6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []))), in(6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ [])), 6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])] = 6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []) = cartesian_product2(9 ^ [], 11 ^ [])],extension(5,bind([[_7953, _8020, _8086, _8151], [6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], 6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])]]))).
% 1.10/1.47 cnf('1.1.1.3.2.1',plain,[-(in(6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []))), -(subset(cartesian_product2(9 ^ [], 11 ^ []), cartesian_product2(10 ^ [], 11 ^ [])))],extension(10,bind([[_13175, _13231], [cartesian_product2(9 ^ [], 11 ^ []), cartesian_product2(10 ^ [], 11 ^ [])]]))).
% 1.10/1.47 cnf('1.1.1.3.2.1.1',plain,[subset(cartesian_product2(9 ^ [], 11 ^ []), cartesian_product2(10 ^ [], 11 ^ []))],reduction('1')).
% 1.10/1.47 cnf('1.1.1.3.2.2',plain,[-(6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])] = 6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])])],extension(4,bind([[_6716], [6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])]]]))).
% 1.10/1.47 cnf('1.1.1.3.2.3',plain,[-(cartesian_product2(9 ^ [], 11 ^ []) = cartesian_product2(9 ^ [], 11 ^ []))],extension(4,bind([[_6716], [cartesian_product2(9 ^ [], 11 ^ [])]]))).
% 1.10/1.47 cnf('1.1.1.4',plain,[-(6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])] = ordered_pair(1 ^ [6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []), 11 ^ [], 9 ^ []], 2 ^ [6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []), 11 ^ [], 9 ^ []])), cartesian_product2(9 ^ [], 11 ^ []) = cartesian_product2(9 ^ [], 11 ^ []), in(6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []))],extension(8,bind([[_12148, _12237, _12508, _12325], [9 ^ [], 11 ^ [], 6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ [])]]))).
% 1.10/1.47 cnf('1.1.1.4.1',plain,[-(cartesian_product2(9 ^ [], 11 ^ []) = cartesian_product2(9 ^ [], 11 ^ [])), 9 ^ [] = 9 ^ [], 11 ^ [] = 11 ^ []],extension(3,bind([[_9236, _9303, _9369, _9434], [9 ^ [], 9 ^ [], 11 ^ [], 11 ^ []]]))).
% 1.10/1.47 cnf('1.1.1.4.1.1',plain,[-(9 ^ [] = 9 ^ [])],extension(4,bind([[_6716], [9 ^ []]]))).
% 1.10/1.47 cnf('1.1.1.4.1.2',plain,[-(11 ^ [] = 11 ^ [])],extension(4,bind([[_6716], [11 ^ []]]))).
% 1.10/1.47 cnf('1.1.1.4.2',plain,[-(in(6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []))), in(6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ [])), 6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])] = 6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []) = cartesian_product2(9 ^ [], 11 ^ [])],extension(5,bind([[_7953, _8020, _8086, _8151], [6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], 6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])]]))).
% 1.10/1.47 cnf('1.1.1.4.2.1',plain,[-(in(6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])], cartesian_product2(9 ^ [], 11 ^ []))), -(subset(cartesian_product2(9 ^ [], 11 ^ []), cartesian_product2(10 ^ [], 11 ^ [])))],extension(10,bind([[_13175, _13231], [cartesian_product2(9 ^ [], 11 ^ []), cartesian_product2(10 ^ [], 11 ^ [])]]))).
% 1.10/1.47 cnf('1.1.1.4.2.1.1',plain,[subset(cartesian_product2(9 ^ [], 11 ^ []), cartesian_product2(10 ^ [], 11 ^ []))],reduction('1')).
% 1.10/1.47 cnf('1.1.1.4.2.2',plain,[-(6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])] = 6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])])],extension(4,bind([[_6716], [6 ^ [cartesian_product2(10 ^ [], 11 ^ []), cartesian_product2(9 ^ [], 11 ^ [])]]]))).
% 1.10/1.47 cnf('1.1.1.4.2.3',plain,[-(cartesian_product2(9 ^ [], 11 ^ []) = cartesian_product2(9 ^ [], 11 ^ []))],extension(4,bind([[_6716], [cartesian_product2(9 ^ [], 11 ^ [])]]))).
% 1.10/1.47 cnf('1.2',plain,[-(subset(cartesian_product2(11 ^ [], 9 ^ []), cartesian_product2(11 ^ [], 10 ^ []))), in(6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 10 ^ []))],extension(11,bind([[_13175, _13231], [cartesian_product2(11 ^ [], 9 ^ []), cartesian_product2(11 ^ [], 10 ^ [])]]))).
% 1.10/1.47 cnf('1.2.1',plain,[-(in(6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 10 ^ []))), cartesian_product2(11 ^ [], 10 ^ []) = cartesian_product2(11 ^ [], 10 ^ []), in(1 ^ [6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []), 9 ^ [], 11 ^ []], 11 ^ []), in(2 ^ [6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []), 9 ^ [], 11 ^ []], 10 ^ []), 6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])] = ordered_pair(1 ^ [6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []), 9 ^ [], 11 ^ []], 2 ^ [6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []), 9 ^ [], 11 ^ []])],extension(9,bind([[_12325, _12148, _12237, _12508, _12645, _12716], [cartesian_product2(11 ^ [], 10 ^ []), 11 ^ [], 10 ^ [], 6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], 1 ^ [6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []), 9 ^ [], 11 ^ []], 2 ^ [6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []), 9 ^ [], 11 ^ []]]]))).
% 1.10/1.47 cnf('1.2.1.1',plain,[-(cartesian_product2(11 ^ [], 10 ^ []) = cartesian_product2(11 ^ [], 10 ^ [])), 11 ^ [] = 11 ^ [], 10 ^ [] = 10 ^ []],extension(3,bind([[_9236, _9303, _9369, _9434], [11 ^ [], 11 ^ [], 10 ^ [], 10 ^ []]]))).
% 1.10/1.47 cnf('1.2.1.1.1',plain,[-(11 ^ [] = 11 ^ [])],extension(4,bind([[_6716], [11 ^ []]]))).
% 1.10/1.47 cnf('1.2.1.1.2',plain,[-(10 ^ [] = 10 ^ [])],extension(4,bind([[_6716], [10 ^ []]]))).
% 1.10/1.47 cnf('1.2.1.2',plain,[-(in(1 ^ [6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []), 9 ^ [], 11 ^ []], 11 ^ [])), cartesian_product2(11 ^ [], 9 ^ []) = cartesian_product2(11 ^ [], 9 ^ []), in(6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []))],extension(6,bind([[_12148, _12237, _12508, _12325], [11 ^ [], 9 ^ [], 6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ [])]]))).
% 1.10/1.47 cnf('1.2.1.2.1',plain,[-(cartesian_product2(11 ^ [], 9 ^ []) = cartesian_product2(11 ^ [], 9 ^ [])), 11 ^ [] = 11 ^ [], 9 ^ [] = 9 ^ []],extension(3,bind([[_9236, _9303, _9369, _9434], [11 ^ [], 11 ^ [], 9 ^ [], 9 ^ []]]))).
% 1.10/1.47 cnf('1.2.1.2.1.1',plain,[-(11 ^ [] = 11 ^ [])],extension(4,bind([[_6716], [11 ^ []]]))).
% 1.10/1.47 cnf('1.2.1.2.1.2',plain,[-(9 ^ [] = 9 ^ [])],extension(4,bind([[_6716], [9 ^ []]]))).
% 1.10/1.47 cnf('1.2.1.2.2',plain,[-(in(6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []))), in(6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ [])), 6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])] = 6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []) = cartesian_product2(11 ^ [], 9 ^ [])],extension(5,bind([[_7953, _8020, _8086, _8151], [6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], 6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []), cartesian_product2(11 ^ [], 9 ^ [])]]))).
% 1.10/1.47 cnf('1.2.1.2.2.1',plain,[-(in(6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []))), -(subset(cartesian_product2(11 ^ [], 9 ^ []), cartesian_product2(11 ^ [], 10 ^ [])))],extension(10,bind([[_13175, _13231], [cartesian_product2(11 ^ [], 9 ^ []), cartesian_product2(11 ^ [], 10 ^ [])]]))).
% 1.10/1.47 cnf('1.2.1.2.2.1.1',plain,[subset(cartesian_product2(11 ^ [], 9 ^ []), cartesian_product2(11 ^ [], 10 ^ []))],reduction('1')).
% 1.10/1.47 cnf('1.2.1.2.2.2',plain,[-(6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])] = 6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])])],extension(4,bind([[_6716], [6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])]]]))).
% 1.10/1.47 cnf('1.2.1.2.2.3',plain,[-(cartesian_product2(11 ^ [], 9 ^ []) = cartesian_product2(11 ^ [], 9 ^ []))],extension(4,bind([[_6716], [cartesian_product2(11 ^ [], 9 ^ [])]]))).
% 1.10/1.47 cnf('1.2.1.3',plain,[-(in(2 ^ [6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []), 9 ^ [], 11 ^ []], 10 ^ [])), subset(9 ^ [], 10 ^ []), in(2 ^ [6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []), 9 ^ [], 11 ^ []], 9 ^ [])],extension(12,bind([[_13231, _13345, _13175], [10 ^ [], 2 ^ [6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []), 9 ^ [], 11 ^ []], 9 ^ []]]))).
% 1.10/1.47 cnf('1.2.1.3.1',plain,[-(subset(9 ^ [], 10 ^ []))],extension(1)).
% 1.10/1.47 cnf('1.2.1.3.2',plain,[-(in(2 ^ [6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []), 9 ^ [], 11 ^ []], 9 ^ [])), cartesian_product2(11 ^ [], 9 ^ []) = cartesian_product2(11 ^ [], 9 ^ []), in(6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []))],extension(7,bind([[_12148, _12237, _12508, _12325], [11 ^ [], 9 ^ [], 6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ [])]]))).
% 1.10/1.47 cnf('1.2.1.3.2.1',plain,[-(cartesian_product2(11 ^ [], 9 ^ []) = cartesian_product2(11 ^ [], 9 ^ []))],extension(4,bind([[_6716], [cartesian_product2(11 ^ [], 9 ^ [])]]))).
% 1.10/1.47 cnf('1.2.1.3.2.2',plain,[-(in(6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []))), -(subset(cartesian_product2(11 ^ [], 9 ^ []), cartesian_product2(11 ^ [], 10 ^ [])))],extension(10,bind([[_13175, _13231], [cartesian_product2(11 ^ [], 9 ^ []), cartesian_product2(11 ^ [], 10 ^ [])]]))).
% 1.10/1.47 cnf('1.2.1.3.2.2.1',plain,[subset(cartesian_product2(11 ^ [], 9 ^ []), cartesian_product2(11 ^ [], 10 ^ []))],reduction('1')).
% 1.10/1.47 cnf('1.2.1.4',plain,[-(6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])] = ordered_pair(1 ^ [6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []), 9 ^ [], 11 ^ []], 2 ^ [6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []), 9 ^ [], 11 ^ []])), cartesian_product2(11 ^ [], 9 ^ []) = cartesian_product2(11 ^ [], 9 ^ []), in(6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []))],extension(8,bind([[_12148, _12237, _12508, _12325], [11 ^ [], 9 ^ [], 6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ [])]]))).
% 1.10/1.47 cnf('1.2.1.4.1',plain,[-(cartesian_product2(11 ^ [], 9 ^ []) = cartesian_product2(11 ^ [], 9 ^ [])), 11 ^ [] = 11 ^ [], 9 ^ [] = 9 ^ []],extension(3,bind([[_9236, _9303, _9369, _9434], [11 ^ [], 11 ^ [], 9 ^ [], 9 ^ []]]))).
% 1.10/1.47 cnf('1.2.1.4.1.1',plain,[-(11 ^ [] = 11 ^ [])],extension(4,bind([[_6716], [11 ^ []]]))).
% 1.10/1.47 cnf('1.2.1.4.1.2',plain,[-(9 ^ [] = 9 ^ [])],extension(4,bind([[_6716], [9 ^ []]]))).
% 1.10/1.47 cnf('1.2.1.4.2',plain,[-(in(6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []))), in(6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ [])), 6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])] = 6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []) = cartesian_product2(11 ^ [], 9 ^ [])],extension(5,bind([[_7953, _8020, _8086, _8151], [6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], 6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []), cartesian_product2(11 ^ [], 9 ^ [])]]))).
% 1.10/1.47 cnf('1.2.1.4.2.1',plain,[-(in(6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])], cartesian_product2(11 ^ [], 9 ^ []))), -(subset(cartesian_product2(11 ^ [], 9 ^ []), cartesian_product2(11 ^ [], 10 ^ [])))],extension(10,bind([[_13175, _13231], [cartesian_product2(11 ^ [], 9 ^ []), cartesian_product2(11 ^ [], 10 ^ [])]]))).
% 1.10/1.47 cnf('1.2.1.4.2.1.1',plain,[subset(cartesian_product2(11 ^ [], 9 ^ []), cartesian_product2(11 ^ [], 10 ^ []))],reduction('1')).
% 1.10/1.47 cnf('1.2.1.4.2.2',plain,[-(6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])] = 6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])])],extension(4,bind([[_6716], [6 ^ [cartesian_product2(11 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 9 ^ [])]]]))).
% 1.10/1.47 cnf('1.2.1.4.2.3',plain,[-(cartesian_product2(11 ^ [], 9 ^ []) = cartesian_product2(11 ^ [], 9 ^ []))],extension(4,bind([[_6716], [cartesian_product2(11 ^ [], 9 ^ [])]]))).
% 1.10/1.47 %-----------------------------------------------------
% 1.10/1.47
% 1.10/1.47 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------