%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET955+1 : TPTP v8.1.0. Bugfixed v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n026.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 02:57:19 EDT 2022
% Result : Theorem 4.20s 4.72s
% Output : Proof 4.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.17 % Problem : SET955+1 : TPTP v8.1.0. Bugfixed v4.0.0.
% 0.08/0.17 % Command : leancop_casc.sh %s %d
% 0.08/0.36 % Computer : n026.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8042.1875MB
% 0.08/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 600
% 0.08/0.36 % DateTime : Sun Jul 10 21:52:41 EDT 2022
% 0.08/0.38 % CPUTime :
% 4.20/4.72 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.20/4.74 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.20/4.75
% 4.20/4.75 %-----------------------------------------------------
% 4.20/4.75 fof(t108_zfmisc_1, conjecture, ! [_50849, _50852, _50855, _50858] : (! [_50866, _50869] : (in(ordered_pair(_50866, _50869), cartesian_product2(_50849, _50852)) <=> in(ordered_pair(_50866, _50869), cartesian_product2(_50855, _50858))) => cartesian_product2(_50849, _50852) = cartesian_product2(_50855, _50858)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t108_zfmisc_1)).
% 4.20/4.75 fof(t2_tarski, axiom, ! [_51206, _51209] : (! [_51217] : (in(_51217, _51206) <=> in(_51217, _51209)) => _51206 = _51209), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t2_tarski)).
% 4.20/4.75 fof(d2_zfmisc_1, axiom, ! [_51418, _51421, _51424] : (_51424 = cartesian_product2(_51418, _51421) <=> ! [_51445] : (in(_51445, _51424) <=> ? [_51463, _51466] : (in(_51463, _51418) & in(_51466, _51421) & _51445 = ordered_pair(_51463, _51466)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d2_zfmisc_1)).
% 4.20/4.75
% 4.20/4.75 cnf(1, plain, [cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])], clausify(t108_zfmisc_1)).
% 4.20/4.75 cnf(2, plain, [in(ordered_pair(_17531, _17536), cartesian_product2(9 ^ [], 10 ^ [])), -(in(ordered_pair(_17531, _17536), cartesian_product2(11 ^ [], 12 ^ [])))], clausify(t108_zfmisc_1)).
% 4.20/4.75 cnf(3, plain, [-(in(ordered_pair(_17531, _17536), cartesian_product2(9 ^ [], 10 ^ []))), in(ordered_pair(_17531, _17536), cartesian_product2(11 ^ [], 12 ^ []))], clausify(t108_zfmisc_1)).
% 4.20/4.75 cnf(4, plain, [-(_13085 = _13141), in(8 ^ [_13141, _13085], _13085), in(8 ^ [_13141, _13085], _13141)], clausify(t2_tarski)).
% 4.20/4.75 cnf(5, plain, [-(_13085 = _13141), -(in(8 ^ [_13141, _13085], _13085)), -(in(8 ^ [_13141, _13085], _13141))], clausify(t2_tarski)).
% 4.20/4.75 cnf(6, plain, [_11284 = cartesian_product2(_11107, _11196), in(_11467, _11284), -(in(1 ^ [_11467, _11284, _11196, _11107], _11107))], clausify(d2_zfmisc_1)).
% 4.20/4.75 cnf(7, plain, [_11284 = cartesian_product2(_11107, _11196), in(_11467, _11284), -(in(2 ^ [_11467, _11284, _11196, _11107], _11196))], clausify(d2_zfmisc_1)).
% 4.20/4.75 cnf(8, plain, [_11284 = cartesian_product2(_11107, _11196), in(_11467, _11284), -(_11467 = ordered_pair(1 ^ [_11467, _11284, _11196, _11107], 2 ^ [_11467, _11284, _11196, _11107]))], clausify(d2_zfmisc_1)).
% 4.20/4.75 cnf(9, plain, [_11284 = cartesian_product2(_11107, _11196), -(in(_11467, _11284)), in(_11604, _11107), in(_11675, _11196), _11467 = ordered_pair(_11604, _11675)], clausify(d2_zfmisc_1)).
% 4.20/4.75 cnf(10, plain, [-(_6314 = _6314)], theory(equality)).
% 4.20/4.75 cnf(11, plain, [_6467 = _6512, -(_6512 = _6467)], theory(equality)).
% 4.20/4.75 cnf(12, plain, [-(in(_7608, _7739)), in(_7541, _7674), _7541 = _7608, _7674 = _7739], theory(equality)).
% 4.20/4.75
% 4.20/4.75 cnf('1',plain,[cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])],start(1)).
% 4.20/4.75 cnf('1.1',plain,[-(cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])), in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ [])), in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []))],extension(4,bind([[_13085, _13141], [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 12 ^ [])]]))).
% 4.20/4.75 cnf('1.1.1',plain,[-(in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []))), in(ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]), cartesian_product2(9 ^ [], 10 ^ [])), ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]) = 8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(9 ^ [], 10 ^ [])],extension(12,bind([[_7541, _7608, _7674, _7739], [ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]), 8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])]]))).
% 4.20/4.75 cnf('1.1.1.1',plain,[-(in(ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]), cartesian_product2(9 ^ [], 10 ^ []))), in(ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]), cartesian_product2(11 ^ [], 12 ^ []))],extension(3,bind([[_17531, _17536], [1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]]]))).
% 4.20/4.75 cnf('1.1.1.1.1',plain,[-(in(ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]), cartesian_product2(11 ^ [], 12 ^ []))), cartesian_product2(11 ^ [], 12 ^ []) = cartesian_product2(11 ^ [], 12 ^ []), in(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 11 ^ []), in(2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 12 ^ []), ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]) = ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []])],extension(9,bind([[_11284, _11107, _11196, _11467, _11604, _11675], [cartesian_product2(11 ^ [], 12 ^ []), 11 ^ [], 12 ^ [], ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]), 1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]]]))).
% 4.20/4.75 cnf('1.1.1.1.1.1',plain,[-(cartesian_product2(11 ^ [], 12 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])), in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])], cartesian_product2(11 ^ [], 12 ^ [])), in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])], cartesian_product2(11 ^ [], 12 ^ []))],extension(4,bind([[_13085, _13141], [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])]]))).
% 4.20/4.75 cnf('1.1.1.1.1.1.1',plain,[-(in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])], cartesian_product2(11 ^ [], 12 ^ []))), -(cartesian_product2(11 ^ [], 12 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])), -(in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])], cartesian_product2(11 ^ [], 12 ^ [])))],extension(5,bind([[_13085, _13141], [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])]]))).
% 4.20/4.75 cnf('1.1.1.1.1.1.1.1',plain,[cartesian_product2(11 ^ [], 12 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])],reduction('1.1.1.1.1')).
% 4.20/4.75 cnf('1.1.1.1.1.1.1.2',plain,[in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])], cartesian_product2(11 ^ [], 12 ^ []))],reduction('1.1.1.1.1.1')).
% 4.20/4.75 cnf('1.1.1.1.1.1.2',plain,[-(in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])], cartesian_product2(11 ^ [], 12 ^ [])))],lemmata('1.1.1.1.1.1')).
% 4.20/4.75 cnf('1.1.1.1.1.2',plain,[-(in(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 11 ^ [])), cartesian_product2(11 ^ [], 12 ^ []) = cartesian_product2(11 ^ [], 12 ^ []), in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []))],extension(6,bind([[_11107, _11196, _11467, _11284], [11 ^ [], 12 ^ [], 8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ [])]]))).
% 4.20/4.75 cnf('1.1.1.1.1.2.1',plain,[-(cartesian_product2(11 ^ [], 12 ^ []) = cartesian_product2(11 ^ [], 12 ^ []))],extension(10,bind([[_6314], [cartesian_product2(11 ^ [], 12 ^ [])]]))).
% 4.20/4.75 cnf('1.1.1.1.1.2.2',plain,[-(in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []))), -(cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])), -(in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ [])))],extension(5,bind([[_13141, _13085], [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])]]))).
% 4.20/4.75 cnf('1.1.1.1.1.2.2.1',plain,[cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])],extension(1)).
% 4.20/4.75 cnf('1.1.1.1.1.2.2.2',plain,[in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []))],reduction('1.1')).
% 4.20/4.75 cnf('1.1.1.1.1.3',plain,[-(in(2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 12 ^ [])), cartesian_product2(11 ^ [], 12 ^ []) = cartesian_product2(11 ^ [], 12 ^ []), in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []))],extension(7,bind([[_11107, _11196, _11467, _11284], [11 ^ [], 12 ^ [], 8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ [])]]))).
% 4.20/4.75 cnf('1.1.1.1.1.3.1',plain,[-(cartesian_product2(11 ^ [], 12 ^ []) = cartesian_product2(11 ^ [], 12 ^ []))],extension(10,bind([[_6314], [cartesian_product2(11 ^ [], 12 ^ [])]]))).
% 4.20/4.75 cnf('1.1.1.1.1.3.2',plain,[-(in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []))), -(cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])), -(in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ [])))],extension(5,bind([[_13141, _13085], [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])]]))).
% 4.20/4.75 cnf('1.1.1.1.1.3.2.1',plain,[cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])],extension(1)).
% 4.20/4.75 cnf('1.1.1.1.1.3.2.2',plain,[in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []))],reduction('1.1')).
% 4.20/4.75 cnf('1.1.1.1.1.4',plain,[-(ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]) = ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []])), in(8 ^ [ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]), ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []])], ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []])), in(8 ^ [ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]), ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []])], ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]))],extension(4,bind([[_13085, _13141], [ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]), ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []])]]))).
% 4.20/4.75 cnf('1.1.1.1.1.4.1',plain,[-(in(8 ^ [ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]), ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []])], ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]))), -(ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]) = ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []])), -(in(8 ^ [ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]), ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []])], ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []])))],extension(5,bind([[_13085, _13141], [ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]), ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []])]]))).
% 4.20/4.75 cnf('1.1.1.1.1.4.1.1',plain,[ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]) = ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []])],reduction('1.1.1.1.1')).
% 4.20/4.75 cnf('1.1.1.1.1.4.1.2',plain,[in(8 ^ [ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]), ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []])], ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]))],reduction('1.1.1.1.1.4')).
% 4.20/4.75 cnf('1.1.1.1.1.4.2',plain,[-(in(8 ^ [ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]), ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []])], ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []])))],lemmata('1.1.1.1.1.4')).
% 4.20/4.75 cnf('1.1.1.2',plain,[-(ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []]) = 8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])]), 8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])] = ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []])],extension(11,bind([[_6467, _6512], [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []])]]))).
% 4.20/4.75 cnf('1.1.1.2.1',plain,[-(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])] = ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), 12 ^ [], 11 ^ []])), cartesian_product2(11 ^ [], 12 ^ []) = cartesian_product2(11 ^ [], 12 ^ []), in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []))],extension(8,bind([[_11107, _11196, _11467, _11284], [11 ^ [], 12 ^ [], 8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ [])]]))).
% 4.20/4.75 cnf('1.1.1.2.1.1',plain,[-(cartesian_product2(11 ^ [], 12 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])), in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])], cartesian_product2(11 ^ [], 12 ^ [])), in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])], cartesian_product2(11 ^ [], 12 ^ []))],extension(4,bind([[_13085, _13141], [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])]]))).
% 4.20/4.75 cnf('1.1.1.2.1.1.1',plain,[-(in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])], cartesian_product2(11 ^ [], 12 ^ []))), -(cartesian_product2(11 ^ [], 12 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])), -(in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])], cartesian_product2(11 ^ [], 12 ^ [])))],extension(5,bind([[_13085, _13141], [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])]]))).
% 4.20/4.75 cnf('1.1.1.2.1.1.1.1',plain,[cartesian_product2(11 ^ [], 12 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])],reduction('1.1.1.2.1')).
% 4.20/4.75 cnf('1.1.1.2.1.1.1.2',plain,[in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])], cartesian_product2(11 ^ [], 12 ^ []))],reduction('1.1.1.2.1.1')).
% 4.20/4.75 cnf('1.1.1.2.1.1.2',plain,[-(in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])], cartesian_product2(11 ^ [], 12 ^ [])))],lemmata('1.1.1.2.1.1')).
% 4.20/4.75 cnf('1.1.1.2.1.2',plain,[-(in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []))), -(cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])), -(in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ [])))],extension(5,bind([[_13141, _13085], [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])]]))).
% 4.20/4.75 cnf('1.1.1.2.1.2.1',plain,[cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])],extension(1)).
% 4.20/4.75 cnf('1.1.1.2.1.2.2',plain,[in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []))],reduction('1.1')).
% 4.20/4.75 cnf('1.1.1.3',plain,[-(cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(9 ^ [], 10 ^ [])), in(8 ^ [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ [])), in(8 ^ [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []))],extension(4,bind([[_13085, _13141], [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])]]))).
% 4.20/4.75 cnf('1.1.1.3.1',plain,[-(in(8 ^ [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []))), -(cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(9 ^ [], 10 ^ [])), -(in(8 ^ [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ [])))],extension(5,bind([[_13085, _13141], [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])]]))).
% 4.20/4.75 cnf('1.1.1.3.1.1',plain,[cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(9 ^ [], 10 ^ [])],reduction('1.1.1')).
% 4.20/4.75 cnf('1.1.1.3.1.2',plain,[in(8 ^ [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []))],reduction('1.1.1.3')).
% 4.20/4.75 cnf('1.1.1.3.2',plain,[-(in(8 ^ [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ [])))],lemmata('1.1.1.3')).
% 4.20/4.75 cnf('1.1.2',plain,[-(in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []))), in(ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]), cartesian_product2(11 ^ [], 12 ^ [])), ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]) = 8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])],extension(12,bind([[_7541, _7608, _7674, _7739], [ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]), 8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])]]))).
% 4.20/4.75 cnf('1.1.2.1',plain,[-(in(ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]), cartesian_product2(11 ^ [], 12 ^ []))), in(ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]), cartesian_product2(9 ^ [], 10 ^ []))],extension(2,bind([[_17531, _17536], [1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]]]))).
% 4.20/4.75 cnf('1.1.2.1.1',plain,[-(in(ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]), cartesian_product2(9 ^ [], 10 ^ []))), cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(9 ^ [], 10 ^ []), in(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 9 ^ []), in(2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 10 ^ []), ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]) = ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []])],extension(9,bind([[_11284, _11107, _11196, _11467, _11604, _11675], [cartesian_product2(9 ^ [], 10 ^ []), 9 ^ [], 10 ^ [], ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]), 1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]]]))).
% 4.20/4.75 cnf('1.1.2.1.1.1',plain,[-(cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(9 ^ [], 10 ^ [])), in(8 ^ [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ [])), in(8 ^ [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []))],extension(4,bind([[_13085, _13141], [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])]]))).
% 4.20/4.75 cnf('1.1.2.1.1.1.1',plain,[-(in(8 ^ [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []))), -(cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(9 ^ [], 10 ^ [])), -(in(8 ^ [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ [])))],extension(5,bind([[_13085, _13141], [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])]]))).
% 4.20/4.75 cnf('1.1.2.1.1.1.1.1',plain,[cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(9 ^ [], 10 ^ [])],reduction('1.1.2.1.1')).
% 4.20/4.75 cnf('1.1.2.1.1.1.1.2',plain,[in(8 ^ [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []))],reduction('1.1.2.1.1.1')).
% 4.20/4.75 cnf('1.1.2.1.1.1.2',plain,[-(in(8 ^ [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ [])))],lemmata('1.1.2.1.1.1')).
% 4.20/4.75 cnf('1.1.2.1.1.2',plain,[-(in(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 9 ^ [])), cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(9 ^ [], 10 ^ []), in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []))],extension(6,bind([[_11107, _11196, _11467, _11284], [9 ^ [], 10 ^ [], 8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ [])]]))).
% 4.20/4.75 cnf('1.1.2.1.1.2.1',plain,[-(cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(9 ^ [], 10 ^ []))],extension(10,bind([[_6314], [cartesian_product2(9 ^ [], 10 ^ [])]]))).
% 4.20/4.75 cnf('1.1.2.1.1.2.2',plain,[-(in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []))), -(cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])), -(in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ [])))],extension(5,bind([[_13085, _13141], [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 12 ^ [])]]))).
% 4.20/4.75 cnf('1.1.2.1.1.2.2.1',plain,[cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])],extension(1)).
% 4.20/4.75 cnf('1.1.2.1.1.2.2.2',plain,[in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []))],reduction('1.1')).
% 4.20/4.75 cnf('1.1.2.1.1.3',plain,[-(in(2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 10 ^ [])), cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(9 ^ [], 10 ^ []), in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []))],extension(7,bind([[_11107, _11196, _11467, _11284], [9 ^ [], 10 ^ [], 8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ [])]]))).
% 4.20/4.75 cnf('1.1.2.1.1.3.1',plain,[-(cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(9 ^ [], 10 ^ []))],extension(10,bind([[_6314], [cartesian_product2(9 ^ [], 10 ^ [])]]))).
% 4.20/4.75 cnf('1.1.2.1.1.3.2',plain,[-(in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []))), -(cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])), -(in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ [])))],extension(5,bind([[_13085, _13141], [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(11 ^ [], 12 ^ [])]]))).
% 4.20/4.75 cnf('1.1.2.1.1.3.2.1',plain,[cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])],extension(1)).
% 4.20/4.75 cnf('1.1.2.1.1.3.2.2',plain,[in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(11 ^ [], 12 ^ []))],reduction('1.1')).
% 4.20/4.75 cnf('1.1.2.1.1.4',plain,[-(ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]) = ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []])), in(8 ^ [ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]), ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []])], ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []])), in(8 ^ [ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]), ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []])], ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]))],extension(4,bind([[_13085, _13141], [ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]), ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []])]]))).
% 4.20/4.75 cnf('1.1.2.1.1.4.1',plain,[-(in(8 ^ [ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]), ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []])], ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]))), -(ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]) = ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []])), -(in(8 ^ [ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]), ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []])], ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []])))],extension(5,bind([[_13085, _13141], [ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]), ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []])]]))).
% 4.20/4.75 cnf('1.1.2.1.1.4.1.1',plain,[ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]) = ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []])],reduction('1.1.2.1.1')).
% 4.20/4.75 cnf('1.1.2.1.1.4.1.2',plain,[in(8 ^ [ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]), ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []])], ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]))],reduction('1.1.2.1.1.4')).
% 4.20/4.75 cnf('1.1.2.1.1.4.2',plain,[-(in(8 ^ [ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]), ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []])], ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []])))],lemmata('1.1.2.1.1.4')).
% 4.20/4.75 cnf('1.1.2.2',plain,[-(ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []]) = 8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])]), 8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])] = ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []])],extension(11,bind([[_6467, _6512], [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []])]]))).
% 4.20/4.75 cnf('1.1.2.2.1',plain,[-(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])] = ordered_pair(1 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []], 2 ^ [8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []), 10 ^ [], 9 ^ []])), cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(9 ^ [], 10 ^ []), in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []))],extension(8,bind([[_11107, _11196, _11467, _11284], [9 ^ [], 10 ^ [], 8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ [])]]))).
% 4.20/4.75 cnf('1.1.2.2.1.1',plain,[-(cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(9 ^ [], 10 ^ [])), in(8 ^ [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ [])), in(8 ^ [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []))],extension(4,bind([[_13085, _13141], [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])]]))).
% 4.20/4.75 cnf('1.1.2.2.1.1.1',plain,[-(in(8 ^ [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []))), -(cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(9 ^ [], 10 ^ [])), -(in(8 ^ [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ [])))],extension(5,bind([[_13085, _13141], [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])]]))).
% 4.20/4.75 cnf('1.1.2.2.1.1.1.1',plain,[cartesian_product2(9 ^ [], 10 ^ []) = cartesian_product2(9 ^ [], 10 ^ [])],reduction('1.1.2.2.1')).
% 4.20/4.75 cnf('1.1.2.2.1.1.1.2',plain,[in(8 ^ [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ []))],reduction('1.1.2.2.1.1')).
% 4.20/4.75 cnf('1.1.2.2.1.1.2',plain,[-(in(8 ^ [cartesian_product2(9 ^ [], 10 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ [])))],lemmata('1.1.2.2.1.1')).
% 4.20/4.75 cnf('1.1.2.2.1.2',plain,[-(in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(9 ^ [], 10 ^ [])], cartesian_product2(9 ^ [], 10 ^ [])))],lemmata('1.1')).
% 4.20/4.75 cnf('1.1.2.3',plain,[-(cartesian_product2(11 ^ [], 12 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])), in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])], cartesian_product2(11 ^ [], 12 ^ [])), in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])], cartesian_product2(11 ^ [], 12 ^ []))],extension(4,bind([[_13085, _13141], [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])]]))).
% 4.20/4.75 cnf('1.1.2.3.1',plain,[-(in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])], cartesian_product2(11 ^ [], 12 ^ []))), -(cartesian_product2(11 ^ [], 12 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])), -(in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])], cartesian_product2(11 ^ [], 12 ^ [])))],extension(5,bind([[_13085, _13141], [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])]]))).
% 4.20/4.75 cnf('1.1.2.3.1.1',plain,[cartesian_product2(11 ^ [], 12 ^ []) = cartesian_product2(11 ^ [], 12 ^ [])],reduction('1.1.2')).
% 4.20/4.75 cnf('1.1.2.3.1.2',plain,[in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])], cartesian_product2(11 ^ [], 12 ^ []))],reduction('1.1.2.3')).
% 4.20/4.75 cnf('1.1.2.3.2',plain,[-(in(8 ^ [cartesian_product2(11 ^ [], 12 ^ []), cartesian_product2(11 ^ [], 12 ^ [])], cartesian_product2(11 ^ [], 12 ^ [])))],lemmata('1.1.2.3')).
% 4.20/4.75 %-----------------------------------------------------
% 4.20/4.76
% 4.20/4.76 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------