%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET992+1 : TPTP v8.1.0. Bugfixed v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n009.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:32 EDT 2022
% Result : Theorem 6.70s 7.60s
% Output : Proof 6.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SET992+1 : TPTP v8.1.0. Bugfixed v4.0.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n009.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Sun Jul 10 05:30:52 EDT 2022
% 0.12/0.33 % CPUTime :
% 6.70/7.60 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.70/7.60 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.70/7.61
% 6.70/7.61 %-----------------------------------------------------
% 6.70/7.61 fof(t14_funct_1, conjecture, ! [_53309, _53312] : (relation(_53312) & function(_53312) => relation_dom(_53312) = singleton(_53309) => relation_rng(_53312) = singleton(apply(_53312, _53309))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t14_funct_1)).
% 6.70/7.61 fof(d1_tarski, axiom, ! [_53658, _53661] : (_53661 = singleton(_53658) <=> ! [_53679] : (in(_53679, _53661) <=> _53679 = _53658)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_tarski)).
% 6.70/7.61 fof(d5_funct_1, axiom, ! [_53899] : (relation(_53899) & function(_53899) => ! [_53921] : (_53921 = relation_rng(_53899) <=> ! [_53939] : (in(_53939, _53921) <=> ? [_53957] : (in(_53957, relation_dom(_53899)) & _53939 = apply(_53899, _53957))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d5_funct_1)).
% 6.70/7.61
% 6.70/7.61 cnf(1, plain, [-(relation(16 ^ []))], clausify(t14_funct_1)).
% 6.70/7.61 cnf(2, plain, [-(function(16 ^ []))], clausify(t14_funct_1)).
% 6.70/7.61 cnf(3, plain, [-(relation_dom(16 ^ []) = singleton(15 ^ []))], clausify(t14_funct_1)).
% 6.70/7.61 cnf(4, plain, [relation_rng(16 ^ []) = singleton(apply(16 ^ [], 15 ^ []))], clausify(t14_funct_1)).
% 6.70/7.61 cnf(5, plain, [-(apply(_17958, _18091) = apply(_18025, _18156)), _17958 = _18025, _18091 = _18156], theory(equality)).
% 6.70/7.61 cnf(6, plain, [_18911 = _18960, -(relation_dom(_18911) = relation_dom(_18960))], theory(equality)).
% 6.70/7.61 cnf(7, plain, [_19240 = _19289, -(relation_rng(_19240) = relation_rng(_19289))], theory(equality)).
% 6.70/7.61 cnf(8, plain, [-(_13767 = _13767)], theory(equality)).
% 6.70/7.61 cnf(9, plain, [-(_14199 = _14310), _14199 = _14255, _14255 = _14310], theory(equality)).
% 6.70/7.61 cnf(10, plain, [-(in(_16024, _16155)), in(_15957, _16090), _15957 = _16024, _16090 = _16155], theory(equality)).
% 6.70/7.61 cnf(11, plain, [_20792 = singleton(_20734), in(_20924, _20792), -(_20924 = _20734)], clausify(d1_tarski)).
% 6.70/7.61 cnf(12, plain, [_20792 = singleton(_20734), -(in(_20924, _20792)), _20924 = _20734], clausify(d1_tarski)).
% 6.70/7.61 cnf(13, plain, [-(_20792 = singleton(_20734)), in(1 ^ [_20792, _20734], _20792), 1 ^ [_20792, _20734] = _20734], clausify(d1_tarski)).
% 6.70/7.61 cnf(14, plain, [-(_20792 = singleton(_20734)), -(in(1 ^ [_20792, _20734], _20792)), -(1 ^ [_20792, _20734] = _20734)], clausify(d1_tarski)).
% 6.70/7.61 cnf(15, plain, [function(_21215), relation(_21215), _21390 = relation_rng(_21215), in(_21538, _21390), -(in(2 ^ [_21538, _21390, _21215], relation_dom(_21215)))], clausify(d5_funct_1)).
% 6.70/7.61 cnf(16, plain, [function(_21215), relation(_21215), _21390 = relation_rng(_21215), in(_21538, _21390), -(_21538 = apply(_21215, 2 ^ [_21538, _21390, _21215]))], clausify(d5_funct_1)).
% 6.70/7.61 cnf(17, plain, [function(_21215), relation(_21215), _21390 = relation_rng(_21215), -(in(_21538, _21390)), in(_21662, relation_dom(_21215)), _21538 = apply(_21215, _21662)], clausify(d5_funct_1)).
% 6.70/7.61
% 6.70/7.61 cnf('1',plain,[relation_rng(16 ^ []) = singleton(apply(16 ^ [], 15 ^ []))],start(4)).
% 6.70/7.61 cnf('1.1',plain,[-(relation_rng(16 ^ []) = singleton(apply(16 ^ [], 15 ^ []))), -(in(1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], relation_rng(16 ^ []))), -(1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])] = apply(16 ^ [], 15 ^ []))],extension(14,bind([[_20792, _20734], [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])]]))).
% 6.70/7.61 cnf('1.1.1',plain,[in(1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], relation_rng(16 ^ [])), function(16 ^ []), relation(16 ^ []), relation_rng(16 ^ []) = relation_rng(16 ^ []), -(in(2 ^ [1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], relation_rng(16 ^ []), 16 ^ []], relation_dom(16 ^ [])))],extension(15,bind([[_21538, _21390, _21215], [1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], relation_rng(16 ^ []), 16 ^ []]]))).
% 6.70/7.61 cnf('1.1.1.1',plain,[-(function(16 ^ []))],extension(2)).
% 6.70/7.61 cnf('1.1.1.2',plain,[-(relation(16 ^ []))],extension(1)).
% 6.70/7.61 cnf('1.1.1.3',plain,[-(relation_rng(16 ^ []) = relation_rng(16 ^ [])), 16 ^ [] = 16 ^ []],extension(7,bind([[_19240, _19289], [16 ^ [], 16 ^ []]]))).
% 6.70/7.61 cnf('1.1.1.3.1',plain,[-(16 ^ [] = 16 ^ [])],extension(8,bind([[_13767], [16 ^ []]]))).
% 6.70/7.61 cnf('1.1.1.4',plain,[in(2 ^ [1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], relation_rng(16 ^ []), 16 ^ []], relation_dom(16 ^ [])), relation_dom(16 ^ []) = singleton(15 ^ []), -(2 ^ [1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], relation_rng(16 ^ []), 16 ^ []] = 15 ^ [])],extension(11,bind([[_20792, _20924, _20734], [relation_dom(16 ^ []), 2 ^ [1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], relation_rng(16 ^ []), 16 ^ []], 15 ^ []]]))).
% 6.70/7.61 cnf('1.1.1.4.1',plain,[-(relation_dom(16 ^ []) = singleton(15 ^ []))],extension(3)).
% 6.70/7.61 cnf('1.1.1.4.2',plain,[2 ^ [1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], relation_rng(16 ^ []), 16 ^ []] = 15 ^ [], -(apply(16 ^ [], 2 ^ [1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], relation_rng(16 ^ []), 16 ^ []]) = apply(16 ^ [], 15 ^ [])), 16 ^ [] = 16 ^ []],extension(5,bind([[_18091, _18156, _17958, _18025], [2 ^ [1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], relation_rng(16 ^ []), 16 ^ []], 15 ^ [], 16 ^ [], 16 ^ []]]))).
% 6.70/7.61 cnf('1.1.1.4.2.1',plain,[apply(16 ^ [], 2 ^ [1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], relation_rng(16 ^ []), 16 ^ []]) = apply(16 ^ [], 15 ^ []), -(1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])] = apply(16 ^ [], 15 ^ [])), 1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])] = apply(16 ^ [], 2 ^ [1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], relation_rng(16 ^ []), 16 ^ []])],extension(9,bind([[_14310, _14199, _14255], [apply(16 ^ [], 15 ^ []), 1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], apply(16 ^ [], 2 ^ [1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], relation_rng(16 ^ []), 16 ^ []])]]))).
% 6.70/7.61 cnf('1.1.1.4.2.1.1',plain,[1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])] = apply(16 ^ [], 15 ^ []), -(relation_rng(16 ^ []) = singleton(apply(16 ^ [], 15 ^ []))), in(1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], relation_rng(16 ^ []))],extension(13,bind([[_20734, _20792], [apply(16 ^ [], 15 ^ []), relation_rng(16 ^ [])]]))).
% 6.70/7.61 cnf('1.1.1.4.2.1.1.1',plain,[relation_rng(16 ^ []) = singleton(apply(16 ^ [], 15 ^ []))],extension(4)).
% 6.70/7.61 cnf('1.1.1.4.2.1.1.2',plain,[-(in(1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], relation_rng(16 ^ [])))],reduction('1.1')).
% 6.70/7.61 cnf('1.1.1.4.2.1.2',plain,[-(1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])] = apply(16 ^ [], 2 ^ [1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], relation_rng(16 ^ []), 16 ^ []])), function(16 ^ []), relation(16 ^ []), relation_rng(16 ^ []) = relation_rng(16 ^ []), in(1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], relation_rng(16 ^ []))],extension(16,bind([[_21215, _21538, _21390], [16 ^ [], 1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], relation_rng(16 ^ [])]]))).
% 6.70/7.61 cnf('1.1.1.4.2.1.2.1',plain,[-(function(16 ^ []))],extension(2)).
% 6.70/7.61 cnf('1.1.1.4.2.1.2.2',plain,[-(relation(16 ^ []))],extension(1)).
% 6.70/7.61 cnf('1.1.1.4.2.1.2.3',plain,[-(relation_rng(16 ^ []) = relation_rng(16 ^ []))],extension(8,bind([[_13767], [relation_rng(16 ^ [])]]))).
% 6.70/7.61 cnf('1.1.1.4.2.1.2.4',plain,[-(in(1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], relation_rng(16 ^ [])))],reduction('1.1')).
% 6.70/7.61 cnf('1.1.1.4.2.2',plain,[-(16 ^ [] = 16 ^ [])],extension(8,bind([[_13767], [16 ^ []]]))).
% 6.70/7.61 cnf('1.1.2',plain,[1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])] = apply(16 ^ [], 15 ^ []), -(relation_rng(16 ^ []) = singleton(apply(16 ^ [], 15 ^ []))), in(1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], relation_rng(16 ^ []))],extension(13,bind([[_20734, _20792], [apply(16 ^ [], 15 ^ []), relation_rng(16 ^ [])]]))).
% 6.70/7.61 cnf('1.1.2.1',plain,[relation_rng(16 ^ []) = singleton(apply(16 ^ [], 15 ^ []))],extension(4)).
% 6.70/7.61 cnf('1.1.2.2',plain,[-(in(1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], relation_rng(16 ^ []))), function(16 ^ []), relation(16 ^ []), relation_rng(16 ^ []) = relation_rng(16 ^ []), in(15 ^ [], relation_dom(16 ^ [])), 1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])] = apply(16 ^ [], 15 ^ [])],extension(17,bind([[_21390, _21538, _21215, _21662], [relation_rng(16 ^ []), 1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])], 16 ^ [], 15 ^ []]]))).
% 6.70/7.61 cnf('1.1.2.2.1',plain,[-(function(16 ^ []))],extension(2)).
% 6.70/7.61 cnf('1.1.2.2.2',plain,[-(relation(16 ^ []))],extension(1)).
% 6.70/7.61 cnf('1.1.2.2.3',plain,[-(relation_rng(16 ^ []) = relation_rng(16 ^ [])), 16 ^ [] = 16 ^ []],extension(7,bind([[_19240, _19289], [16 ^ [], 16 ^ []]]))).
% 6.70/7.61 cnf('1.1.2.2.3.1',plain,[-(16 ^ [] = 16 ^ [])],extension(8,bind([[_13767], [16 ^ []]]))).
% 6.70/7.61 cnf('1.1.2.2.4',plain,[-(in(15 ^ [], relation_dom(16 ^ []))), in(15 ^ [], relation_dom(16 ^ [])), 15 ^ [] = 15 ^ [], relation_dom(16 ^ []) = relation_dom(16 ^ [])],extension(10,bind([[_15957, _16024, _16090, _16155], [15 ^ [], 15 ^ [], relation_dom(16 ^ []), relation_dom(16 ^ [])]]))).
% 6.70/7.61 cnf('1.1.2.2.4.1',plain,[-(in(15 ^ [], relation_dom(16 ^ []))), relation_dom(16 ^ []) = singleton(15 ^ []), 15 ^ [] = 15 ^ []],extension(12,bind([[_20792, _20924, _20734], [relation_dom(16 ^ []), 15 ^ [], 15 ^ []]]))).
% 6.70/7.61 cnf('1.1.2.2.4.1.1',plain,[-(relation_dom(16 ^ []) = singleton(15 ^ []))],extension(3)).
% 6.70/7.61 cnf('1.1.2.2.4.1.2',plain,[-(15 ^ [] = 15 ^ [])],extension(8,bind([[_13767], [15 ^ []]]))).
% 6.70/7.61 cnf('1.1.2.2.4.2',plain,[-(15 ^ [] = 15 ^ [])],extension(8,bind([[_13767], [15 ^ []]]))).
% 6.70/7.61 cnf('1.1.2.2.4.3',plain,[-(relation_dom(16 ^ []) = relation_dom(16 ^ [])), 16 ^ [] = 16 ^ []],extension(6,bind([[_18911, _18960], [16 ^ [], 16 ^ []]]))).
% 6.70/7.61 cnf('1.1.2.2.4.3.1',plain,[-(16 ^ [] = 16 ^ [])],extension(8,bind([[_13767], [16 ^ []]]))).
% 6.70/7.61 cnf('1.1.2.2.5',plain,[-(1 ^ [relation_rng(16 ^ []), apply(16 ^ [], 15 ^ [])] = apply(16 ^ [], 15 ^ []))],reduction('1.1')).
% 6.70/7.61 %-----------------------------------------------------
% 6.70/7.61
% 6.70/7.61 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------