%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET964+1 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n018.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:22 EDT 2022
% Result : Theorem 29.42s 29.34s
% Output : Proof 29.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.01/0.12 % Problem : SET964+1 : TPTP v8.1.0. Released v3.2.0.
% 0.12/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n018.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Sun Jul 10 08:29:27 EDT 2022
% 0.19/0.34 % CPUTime :
% 29.42/29.34 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.42/29.35 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.42/29.35
% 29.42/29.35 %-----------------------------------------------------
% 29.42/29.35 fof(l55_zfmisc_1, axiom, ! [_39660, _39663, _39666, _39669] : (in(ordered_pair(_39660, _39663), cartesian_product2(_39666, _39669)) <=> in(_39660, _39666) & in(_39663, _39669)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l55_zfmisc_1)).
% 29.42/29.35 fof(d3_tarski, axiom, ! [_39899, _39902] : (subset(_39899, _39902) <=> ! [_39920] : (in(_39920, _39899) => in(_39920, _39902))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d3_tarski)).
% 29.42/29.35 fof(d2_zfmisc_1, axiom, ! [_40124, _40127, _40130] : (_40130 = cartesian_product2(_40124, _40127) <=> ! [_40151] : (in(_40151, _40130) <=> ? [_40169, _40172] : (in(_40169, _40124) & in(_40172, _40127) & _40151 = ordered_pair(_40169, _40172)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d2_zfmisc_1)).
% 29.42/29.35 fof(t117_zfmisc_1, conjecture, ! [_40461, _40464, _40467] : ~ ((! _40461) = empty_set & (subset(cartesian_product2(_40464, _40461), cartesian_product2(_40467, _40461)) | subset(cartesian_product2(_40461, _40464), cartesian_product2(_40461, _40467))) & ~ subset(_40464, _40467)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t117_zfmisc_1)).
% 29.42/29.35 fof(d1_xboole_0, axiom, ! [_40782] : (_40782 = empty_set <=> ! [_40796] : ~ in(_40796, _40782)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_xboole_0)).
% 29.42/29.35
% 29.42/29.35 cnf(1, plain, [-(13 ^ [_15644, _15579, _15513, _15446]), -(in(_15513, _15644))], clausify(l55_zfmisc_1)).
% 29.42/29.35 cnf(2, plain, [-(13 ^ [_15644, _15579, _15513, _15446]), -(in(_15446, _15579))], clausify(l55_zfmisc_1)).
% 29.42/29.35 cnf(3, plain, [-(12 ^ [_14292, _14236]), in(11 ^ [_14292, _14236], _14292)], clausify(d3_tarski)).
% 29.42/29.35 cnf(4, plain, [-(12 ^ [_14292, _14236]), -(in(11 ^ [_14292, _14236], _14236))], clausify(d3_tarski)).
% 29.42/29.35 cnf(5, plain, [-(5 ^ [_13386, _13298, _13209]), -(in(_13569, _13386)), in(_13706, _13209), in(_13777, _13298), _13569 = ordered_pair(_13706, _13777)], clausify(d2_zfmisc_1)).
% 29.42/29.35 cnf(6, plain, [16 ^ [] = empty_set], clausify(t117_zfmisc_1)).
% 29.42/29.35 cnf(7, plain, [subset(17 ^ [], 18 ^ [])], clausify(t117_zfmisc_1)).
% 29.42/29.35 cnf(8, plain, [-(subset(cartesian_product2(17 ^ [], 16 ^ []), cartesian_product2(18 ^ [], 16 ^ []))), -(subset(cartesian_product2(16 ^ [], 17 ^ []), cartesian_product2(16 ^ [], 18 ^ [])))], clausify(t117_zfmisc_1)).
% 29.42/29.35 cnf(9, plain, [-(_12885 = empty_set), -(in(1 ^ [_12885], _12885))], clausify(d1_xboole_0)).
% 29.42/29.35 cnf(10, plain, [-(subset(_14236, _14292)), 12 ^ [_14292, _14236]], clausify(d3_tarski)).
% 29.42/29.35 cnf(11, plain, [subset(_14236, _14292), in(_14406, _14236), -(in(_14406, _14292))], clausify(d3_tarski)).
% 29.42/29.35 cnf(12, plain, [in(ordered_pair(_15446, _15513), cartesian_product2(_15579, _15644)), 13 ^ [_15644, _15579, _15513, _15446]], clausify(l55_zfmisc_1)).
% 29.42/29.35 cnf(13, plain, [_13386 = cartesian_product2(_13209, _13298), 5 ^ [_13386, _13298, _13209]], clausify(d2_zfmisc_1)).
% 29.42/29.35 cnf(14, plain, [-(cartesian_product2(_9973, _10106) = cartesian_product2(_10040, _10171)), _9973 = _10040, _10106 = _10171], theory(equality)).
% 29.42/29.35 cnf(15, plain, [-(ordered_pair(_10597, _10730) = ordered_pair(_10664, _10795)), _10597 = _10664, _10730 = _10795], theory(equality)).
% 29.42/29.35 cnf(16, plain, [-(_7453 = _7453)], theory(equality)).
% 29.42/29.35
% 29.42/29.35 cnf('1',plain,[-(subset(cartesian_product2(17 ^ [], 16 ^ []), cartesian_product2(18 ^ [], 16 ^ []))), -(subset(cartesian_product2(16 ^ [], 17 ^ []), cartesian_product2(16 ^ [], 18 ^ [])))],start(8)).
% 29.42/29.35 cnf('1.1',plain,[subset(cartesian_product2(17 ^ [], 16 ^ []), cartesian_product2(18 ^ [], 16 ^ [])), in(ordered_pair(11 ^ [18 ^ [], 17 ^ []], 1 ^ [16 ^ []]), cartesian_product2(17 ^ [], 16 ^ [])), -(in(ordered_pair(11 ^ [18 ^ [], 17 ^ []], 1 ^ [16 ^ []]), cartesian_product2(18 ^ [], 16 ^ [])))],extension(11,bind([[_14236, _14406, _14292], [cartesian_product2(17 ^ [], 16 ^ []), ordered_pair(11 ^ [18 ^ [], 17 ^ []], 1 ^ [16 ^ []]), cartesian_product2(18 ^ [], 16 ^ [])]]))).
% 29.42/29.35 cnf('1.1.1',plain,[-(in(ordered_pair(11 ^ [18 ^ [], 17 ^ []], 1 ^ [16 ^ []]), cartesian_product2(17 ^ [], 16 ^ []))), -(5 ^ [cartesian_product2(17 ^ [], 16 ^ []), 16 ^ [], 17 ^ []]), in(11 ^ [18 ^ [], 17 ^ []], 17 ^ []), in(1 ^ [16 ^ []], 16 ^ []), ordered_pair(11 ^ [18 ^ [], 17 ^ []], 1 ^ [16 ^ []]) = ordered_pair(11 ^ [18 ^ [], 17 ^ []], 1 ^ [16 ^ []])],extension(5,bind([[_13386, _13209, _13298, _13569, _13706, _13777], [cartesian_product2(17 ^ [], 16 ^ []), 17 ^ [], 16 ^ [], ordered_pair(11 ^ [18 ^ [], 17 ^ []], 1 ^ [16 ^ []]), 11 ^ [18 ^ [], 17 ^ []], 1 ^ [16 ^ []]]]))).
% 29.42/29.35 cnf('1.1.1.1',plain,[5 ^ [cartesian_product2(17 ^ [], 16 ^ []), 16 ^ [], 17 ^ []], cartesian_product2(17 ^ [], 16 ^ []) = cartesian_product2(17 ^ [], 16 ^ [])],extension(13,bind([[_13386, _13209, _13298], [cartesian_product2(17 ^ [], 16 ^ []), 17 ^ [], 16 ^ []]]))).
% 29.42/29.35 cnf('1.1.1.1.1',plain,[-(cartesian_product2(17 ^ [], 16 ^ []) = cartesian_product2(17 ^ [], 16 ^ [])), 17 ^ [] = 17 ^ [], 16 ^ [] = 16 ^ []],extension(14,bind([[_9973, _10040, _10106, _10171], [17 ^ [], 17 ^ [], 16 ^ [], 16 ^ []]]))).
% 29.42/29.35 cnf('1.1.1.1.1.1',plain,[-(17 ^ [] = 17 ^ [])],extension(16,bind([[_7453], [17 ^ []]]))).
% 29.42/29.35 cnf('1.1.1.1.1.2',plain,[-(16 ^ [] = 16 ^ [])],extension(16,bind([[_7453], [16 ^ []]]))).
% 29.42/29.35 cnf('1.1.1.2',plain,[-(in(11 ^ [18 ^ [], 17 ^ []], 17 ^ [])), -(12 ^ [18 ^ [], 17 ^ []])],extension(4,bind([[_14292, _14236], [18 ^ [], 17 ^ []]]))).
% 29.42/29.35 cnf('1.1.1.2.1',plain,[12 ^ [18 ^ [], 17 ^ []], -(subset(17 ^ [], 18 ^ []))],extension(10,bind([[_14236, _14292], [17 ^ [], 18 ^ []]]))).
% 29.42/29.35 cnf('1.1.1.2.1.1',plain,[subset(17 ^ [], 18 ^ [])],extension(7)).
% 29.42/29.35 cnf('1.1.1.3',plain,[-(in(1 ^ [16 ^ []], 16 ^ [])), -(16 ^ [] = empty_set)],extension(9,bind([[_12885], [16 ^ []]]))).
% 29.42/29.35 cnf('1.1.1.3.1',plain,[16 ^ [] = empty_set],extension(6)).
% 29.42/29.35 cnf('1.1.1.4',plain,[-(ordered_pair(11 ^ [18 ^ [], 17 ^ []], 1 ^ [16 ^ []]) = ordered_pair(11 ^ [18 ^ [], 17 ^ []], 1 ^ [16 ^ []])), 11 ^ [18 ^ [], 17 ^ []] = 11 ^ [18 ^ [], 17 ^ []], 1 ^ [16 ^ []] = 1 ^ [16 ^ []]],extension(15,bind([[_10597, _10664, _10730, _10795], [11 ^ [18 ^ [], 17 ^ []], 11 ^ [18 ^ [], 17 ^ []], 1 ^ [16 ^ []], 1 ^ [16 ^ []]]]))).
% 29.42/29.35 cnf('1.1.1.4.1',plain,[-(11 ^ [18 ^ [], 17 ^ []] = 11 ^ [18 ^ [], 17 ^ []])],extension(16,bind([[_7453], [11 ^ [18 ^ [], 17 ^ []]]]))).
% 29.42/29.35 cnf('1.1.1.4.2',plain,[-(1 ^ [16 ^ []] = 1 ^ [16 ^ []])],extension(16,bind([[_7453], [1 ^ [16 ^ []]]]))).
% 29.42/29.35 cnf('1.1.2',plain,[in(ordered_pair(11 ^ [18 ^ [], 17 ^ []], 1 ^ [16 ^ []]), cartesian_product2(18 ^ [], 16 ^ [])), 13 ^ [16 ^ [], 18 ^ [], 1 ^ [16 ^ []], 11 ^ [18 ^ [], 17 ^ []]]],extension(12,bind([[_15644, _15579, _15513, _15446], [16 ^ [], 18 ^ [], 1 ^ [16 ^ []], 11 ^ [18 ^ [], 17 ^ []]]]))).
% 29.42/29.35 cnf('1.1.2.1',plain,[-(13 ^ [16 ^ [], 18 ^ [], 1 ^ [16 ^ []], 11 ^ [18 ^ [], 17 ^ []]]), -(in(11 ^ [18 ^ [], 17 ^ []], 18 ^ []))],extension(2,bind([[_15644, _15513, _15446, _15579], [16 ^ [], 1 ^ [16 ^ []], 11 ^ [18 ^ [], 17 ^ []], 18 ^ []]]))).
% 29.42/29.35 cnf('1.1.2.1.1',plain,[in(11 ^ [18 ^ [], 17 ^ []], 18 ^ []), -(12 ^ [18 ^ [], 17 ^ []])],extension(3,bind([[_14292, _14236], [18 ^ [], 17 ^ []]]))).
% 29.42/29.35 cnf('1.1.2.1.1.1',plain,[12 ^ [18 ^ [], 17 ^ []], -(subset(17 ^ [], 18 ^ []))],extension(10,bind([[_14236, _14292], [17 ^ [], 18 ^ []]]))).
% 29.42/29.35 cnf('1.1.2.1.1.1.1',plain,[subset(17 ^ [], 18 ^ [])],extension(7)).
% 29.42/29.35 cnf('1.2',plain,[subset(cartesian_product2(16 ^ [], 17 ^ []), cartesian_product2(16 ^ [], 18 ^ [])), in(ordered_pair(1 ^ [16 ^ []], 11 ^ [18 ^ [], 17 ^ []]), cartesian_product2(16 ^ [], 17 ^ [])), -(in(ordered_pair(1 ^ [16 ^ []], 11 ^ [18 ^ [], 17 ^ []]), cartesian_product2(16 ^ [], 18 ^ [])))],extension(11,bind([[_14236, _14406, _14292], [cartesian_product2(16 ^ [], 17 ^ []), ordered_pair(1 ^ [16 ^ []], 11 ^ [18 ^ [], 17 ^ []]), cartesian_product2(16 ^ [], 18 ^ [])]]))).
% 29.42/29.35 cnf('1.2.1',plain,[-(in(ordered_pair(1 ^ [16 ^ []], 11 ^ [18 ^ [], 17 ^ []]), cartesian_product2(16 ^ [], 17 ^ []))), -(5 ^ [cartesian_product2(16 ^ [], 17 ^ []), 17 ^ [], 16 ^ []]), in(1 ^ [16 ^ []], 16 ^ []), in(11 ^ [18 ^ [], 17 ^ []], 17 ^ []), ordered_pair(1 ^ [16 ^ []], 11 ^ [18 ^ [], 17 ^ []]) = ordered_pair(1 ^ [16 ^ []], 11 ^ [18 ^ [], 17 ^ []])],extension(5,bind([[_13386, _13209, _13298, _13569, _13706, _13777], [cartesian_product2(16 ^ [], 17 ^ []), 16 ^ [], 17 ^ [], ordered_pair(1 ^ [16 ^ []], 11 ^ [18 ^ [], 17 ^ []]), 1 ^ [16 ^ []], 11 ^ [18 ^ [], 17 ^ []]]]))).
% 29.42/29.35 cnf('1.2.1.1',plain,[5 ^ [cartesian_product2(16 ^ [], 17 ^ []), 17 ^ [], 16 ^ []], cartesian_product2(16 ^ [], 17 ^ []) = cartesian_product2(16 ^ [], 17 ^ [])],extension(13,bind([[_13386, _13209, _13298], [cartesian_product2(16 ^ [], 17 ^ []), 16 ^ [], 17 ^ []]]))).
% 29.42/29.35 cnf('1.2.1.1.1',plain,[-(cartesian_product2(16 ^ [], 17 ^ []) = cartesian_product2(16 ^ [], 17 ^ [])), 16 ^ [] = 16 ^ [], 17 ^ [] = 17 ^ []],extension(14,bind([[_9973, _10040, _10106, _10171], [16 ^ [], 16 ^ [], 17 ^ [], 17 ^ []]]))).
% 29.42/29.35 cnf('1.2.1.1.1.1',plain,[-(16 ^ [] = 16 ^ [])],extension(16,bind([[_7453], [16 ^ []]]))).
% 29.42/29.35 cnf('1.2.1.1.1.2',plain,[-(17 ^ [] = 17 ^ [])],extension(16,bind([[_7453], [17 ^ []]]))).
% 29.42/29.35 cnf('1.2.1.2',plain,[-(in(1 ^ [16 ^ []], 16 ^ [])), -(16 ^ [] = empty_set)],extension(9,bind([[_12885], [16 ^ []]]))).
% 29.42/29.35 cnf('1.2.1.2.1',plain,[16 ^ [] = empty_set],extension(6)).
% 29.42/29.35 cnf('1.2.1.3',plain,[-(in(11 ^ [18 ^ [], 17 ^ []], 17 ^ [])), -(12 ^ [18 ^ [], 17 ^ []])],extension(4,bind([[_14292, _14236], [18 ^ [], 17 ^ []]]))).
% 29.42/29.35 cnf('1.2.1.3.1',plain,[12 ^ [18 ^ [], 17 ^ []], -(subset(17 ^ [], 18 ^ []))],extension(10,bind([[_14236, _14292], [17 ^ [], 18 ^ []]]))).
% 29.42/29.35 cnf('1.2.1.3.1.1',plain,[subset(17 ^ [], 18 ^ [])],extension(7)).
% 29.42/29.35 cnf('1.2.1.4',plain,[-(ordered_pair(1 ^ [16 ^ []], 11 ^ [18 ^ [], 17 ^ []]) = ordered_pair(1 ^ [16 ^ []], 11 ^ [18 ^ [], 17 ^ []])), 1 ^ [16 ^ []] = 1 ^ [16 ^ []], 11 ^ [18 ^ [], 17 ^ []] = 11 ^ [18 ^ [], 17 ^ []]],extension(15,bind([[_10597, _10664, _10730, _10795], [1 ^ [16 ^ []], 1 ^ [16 ^ []], 11 ^ [18 ^ [], 17 ^ []], 11 ^ [18 ^ [], 17 ^ []]]]))).
% 29.42/29.35 cnf('1.2.1.4.1',plain,[-(1 ^ [16 ^ []] = 1 ^ [16 ^ []])],extension(16,bind([[_7453], [1 ^ [16 ^ []]]]))).
% 29.42/29.35 cnf('1.2.1.4.2',plain,[-(11 ^ [18 ^ [], 17 ^ []] = 11 ^ [18 ^ [], 17 ^ []])],extension(16,bind([[_7453], [11 ^ [18 ^ [], 17 ^ []]]]))).
% 29.42/29.35 cnf('1.2.2',plain,[in(ordered_pair(1 ^ [16 ^ []], 11 ^ [18 ^ [], 17 ^ []]), cartesian_product2(16 ^ [], 18 ^ [])), 13 ^ [18 ^ [], 16 ^ [], 11 ^ [18 ^ [], 17 ^ []], 1 ^ [16 ^ []]]],extension(12,bind([[_15644, _15579, _15513, _15446], [18 ^ [], 16 ^ [], 11 ^ [18 ^ [], 17 ^ []], 1 ^ [16 ^ []]]]))).
% 29.42/29.35 cnf('1.2.2.1',plain,[-(13 ^ [18 ^ [], 16 ^ [], 11 ^ [18 ^ [], 17 ^ []], 1 ^ [16 ^ []]]), -(in(11 ^ [18 ^ [], 17 ^ []], 18 ^ []))],extension(1,bind([[_15579, _15446, _15513, _15644], [16 ^ [], 1 ^ [16 ^ []], 11 ^ [18 ^ [], 17 ^ []], 18 ^ []]]))).
% 29.42/29.35 cnf('1.2.2.1.1',plain,[in(11 ^ [18 ^ [], 17 ^ []], 18 ^ []), -(12 ^ [18 ^ [], 17 ^ []])],extension(3,bind([[_14292, _14236], [18 ^ [], 17 ^ []]]))).
% 29.42/29.35 cnf('1.2.2.1.1.1',plain,[12 ^ [18 ^ [], 17 ^ []], -(subset(17 ^ [], 18 ^ []))],extension(10,bind([[_14236, _14292], [17 ^ [], 18 ^ []]]))).
% 29.42/29.35 cnf('1.2.2.1.1.1.1',plain,[subset(17 ^ [], 18 ^ [])],extension(7)).
% 29.42/29.35 %-----------------------------------------------------
% 29.51/29.36
% 29.51/29.36 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------