%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : KRS138+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n020.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 : Sun Jul 17 03:13:48 EDT 2022
% Result : Theorem 29.25s 29.29s
% Output : Proof 29.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.11 % Problem : KRS138+1 : TPTP v8.1.0. Released v3.1.0.
% 0.09/0.12 % Command : leancop_casc.sh %s %d
% 0.11/0.32 % Computer : n020.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 600
% 0.11/0.33 % DateTime : Tue Jun 7 10:39:06 EDT 2022
% 0.11/0.33 % CPUTime :
% 29.25/29.29 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.25/29.29 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.25/29.30
% 29.25/29.30 %-----------------------------------------------------
% 29.25/29.30 fof(the_axiom, conjecture, ! [_48247] : (cowlThing(_48247) & ~ cowlNothing(_48247)) & ! [_48247] : (xsd_string(_48247) <=> ~ xsd_integer(_48247)) & ! [_48247, _48296] : (requalityOnA(_48247, _48296) => _48247 = ia | _48247 = ib | _48247 = ic) & ! [_48247, _48296] : (requalityOnA(_48247, _48296) => requalityOnA(_48296, _48247)) & cowlThing(ia) & requalityOnA(ia, ia) & cowlThing(ib) & cowlThing(ic), file('/export/starexec/sandbox/benchmark/theBenchmark.p', the_axiom)).
% 29.25/29.30 fof(requalityOnA_substitution_2, axiom, ! [_48971, _48974, _48977] : (_48971 = _48974 & requalityOnA(_48977, _48971) => requalityOnA(_48977, _48974)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', requalityOnA_substitution_2)).
% 29.25/29.30 fof(axiom_0, axiom, ! [_49154] : (cowlThing(_49154) & ~ cowlNothing(_49154)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_0)).
% 29.25/29.30 fof(axiom_1, axiom, ! [_49294] : (xsd_string(_49294) <=> ~ xsd_integer(_49294)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_1)).
% 29.25/29.30 fof(axiom_2, axiom, ! [_49435] : (cA(_49435) <=> _49435 = ib | _49435 = ia), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 29.25/29.30 fof(axiom_6, axiom, requalityOnA(ia, ia), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_6)).
% 29.25/29.30 fof(axiom_8, axiom, requalityOnA(ib, ib), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_8)).
% 29.25/29.30 fof(axiom_4, axiom, ! [_49686, _49689] : (requalityOnA(_49686, _49689) => cA(_49689)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 29.25/29.30 fof(axiom_3, axiom, ! [_49825, _49828, _49831] : (requalityOnA(_49828, _49825) & requalityOnA(_49831, _49825) => _49828 = _49831), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 29.25/29.30
% 29.25/29.30 cnf(1, plain, [-(11 ^ []), requalityOnA(10 ^ [], 9 ^ [])], clausify(the_axiom)).
% 29.25/29.30 cnf(2, plain, [-(11 ^ []), -(requalityOnA(9 ^ [], 10 ^ []))], clausify(the_axiom)).
% 29.25/29.30 cnf(3, plain, [-(8 ^ []), 6 ^ [] = ib], clausify(the_axiom)).
% 29.25/29.30 cnf(4, plain, [-(8 ^ []), 6 ^ [] = ia], clausify(the_axiom)).
% 29.25/29.30 cnf(5, plain, [-(8 ^ []), -(requalityOnA(6 ^ [], 7 ^ []))], clausify(the_axiom)).
% 29.25/29.30 cnf(6, plain, [-(5 ^ []), xsd_string(3 ^ [])], clausify(the_axiom)).
% 29.25/29.30 cnf(7, plain, [-(5 ^ []), xsd_integer(3 ^ [])], clausify(the_axiom)).
% 29.25/29.30 cnf(8, plain, [-(4 ^ []), -(xsd_integer(3 ^ []))], clausify(the_axiom)).
% 29.25/29.30 cnf(9, plain, [-(4 ^ []), -(xsd_string(3 ^ []))], clausify(the_axiom)).
% 29.25/29.30 cnf(10, plain, [-(cowlNothing(2 ^ [])), cowlThing(2 ^ []), 5 ^ [], 4 ^ [], 8 ^ [], 11 ^ [], cowlThing(ia), requalityOnA(ia, ia), cowlThing(ib), cowlThing(ic)], clausify(the_axiom)).
% 29.25/29.30 cnf(11, plain, [-(_8668 = _8668)], theory(equality)).
% 29.25/29.30 cnf(12, plain, [_8821 = _8866, -(_8866 = _8821)], theory(equality)).
% 29.25/29.30 cnf(13, plain, [-(_9100 = _9211), _9100 = _9156, _9156 = _9211], theory(equality)).
% 29.25/29.30 cnf(14, plain, [-(cA(_9625)), _9576 = _9625, cA(_9576)], theory(equality)).
% 29.25/29.30 cnf(15, plain, [-(cowlNothing(_9954)), _9905 = _9954, cowlNothing(_9905)], theory(equality)).
% 29.25/29.30 cnf(16, plain, [-(requalityOnA(_10630, _10761)), requalityOnA(_10563, _10696), _10563 = _10630, _10696 = _10761], theory(equality)).
% 29.25/29.30 cnf(17, plain, [-(xsd_integer(_11236)), _11187 = _11236, xsd_integer(_11187)], theory(equality)).
% 29.25/29.30 cnf(18, plain, [-(requalityOnA(_13574, _13519)), _13463 = _13519, requalityOnA(_13574, _13463)], clausify(requalityOnA_substitution_2)).
% 29.25/29.30 cnf(19, plain, [-(cowlThing(_14630))], clausify(axiom_0)).
% 29.25/29.30 cnf(20, plain, [cowlNothing(_14630)], clausify(axiom_0)).
% 29.25/29.30 cnf(21, plain, [xsd_string(_14858), xsd_integer(_14858)], clausify(axiom_1)).
% 29.25/29.30 cnf(22, plain, [-(xsd_string(_14858)), -(xsd_integer(_14858))], clausify(axiom_1)).
% 29.25/29.30 cnf(23, plain, [cA(_15086), -(_15086 = ib), -(_15086 = ia)], clausify(axiom_2)).
% 29.25/29.30 cnf(24, plain, [-(requalityOnA(ia, ia))], clausify(axiom_6)).
% 29.25/29.30 cnf(25, plain, [-(requalityOnA(ib, ib))], clausify(axiom_8)).
% 29.25/29.30 cnf(26, plain, [requalityOnA(_15865, _15909), -(cA(_15909))], clausify(axiom_4)).
% 29.25/29.30 cnf(27, plain, [-(_15454 = _15509), requalityOnA(_15454, _15398), requalityOnA(_15509, _15398)], clausify(axiom_3)).
% 29.25/29.30
% 29.25/29.30 cnf('1',plain,[-(cowlNothing(2 ^ [])), cowlThing(2 ^ []), 5 ^ [], 4 ^ [], 8 ^ [], 11 ^ [], cowlThing(ia), requalityOnA(ia, ia), cowlThing(ib), cowlThing(ic)],start(10)).
% 29.25/29.30 cnf('1.1',plain,[cowlNothing(2 ^ []), -(cowlNothing(2 ^ [])), 2 ^ [] = 2 ^ []],extension(15,bind([[_9905, _9954], [2 ^ [], 2 ^ []]]))).
% 29.25/29.30 cnf('1.1.1',plain,[cowlNothing(2 ^ []), -(cowlNothing(2 ^ [])), 2 ^ [] = 2 ^ []],extension(15,bind([[_9905, _9954], [2 ^ [], 2 ^ []]]))).
% 29.25/29.30 cnf('1.1.1.1',plain,[cowlNothing(2 ^ []), -(cowlNothing(2 ^ [])), 2 ^ [] = 2 ^ []],extension(15,bind([[_9905, _9954], [2 ^ [], 2 ^ []]]))).
% 29.25/29.30 cnf('1.1.1.1.1',plain,[cowlNothing(2 ^ []), -(cowlNothing(2 ^ [])), 2 ^ [] = 2 ^ []],extension(15,bind([[_9905, _9954], [2 ^ [], 2 ^ []]]))).
% 29.25/29.30 cnf('1.1.1.1.1.1',plain,[cowlNothing(2 ^ []), -(cowlNothing(2 ^ [])), 2 ^ [] = 2 ^ []],extension(15,bind([[_9905, _9954], [2 ^ [], 2 ^ []]]))).
% 29.25/29.30 cnf('1.1.1.1.1.1.1',plain,[cowlNothing(2 ^ [])],extension(20,bind([[_14630], [2 ^ []]]))).
% 29.25/29.30 cnf('1.1.1.1.1.1.2',plain,[-(2 ^ [] = 2 ^ [])],extension(11,bind([[_8668], [2 ^ []]]))).
% 29.25/29.30 cnf('1.1.1.1.1.2',plain,[-(2 ^ [] = 2 ^ [])],extension(11,bind([[_8668], [2 ^ []]]))).
% 29.25/29.30 cnf('1.1.1.1.2',plain,[-(2 ^ [] = 2 ^ [])],extension(11,bind([[_8668], [2 ^ []]]))).
% 29.25/29.30 cnf('1.1.1.2',plain,[-(2 ^ [] = 2 ^ [])],extension(11,bind([[_8668], [2 ^ []]]))).
% 29.25/29.30 cnf('1.1.2',plain,[-(2 ^ [] = 2 ^ [])],extension(11,bind([[_8668], [2 ^ []]]))).
% 29.25/29.30 cnf('1.2',plain,[-(cowlThing(2 ^ []))],extension(19,bind([[_14630], [2 ^ []]]))).
% 29.25/29.30 cnf('1.3',plain,[-(5 ^ []), xsd_string(3 ^ [])],extension(6)).
% 29.25/29.30 cnf('1.3.1',plain,[-(xsd_string(3 ^ [])), -(xsd_integer(3 ^ []))],extension(22,bind([[_14858], [3 ^ []]]))).
% 29.25/29.30 cnf('1.3.1.1',plain,[xsd_integer(3 ^ []), -(5 ^ [])],extension(7)).
% 29.25/29.30 cnf('1.3.1.1.1',plain,[5 ^ []],reduction('1')).
% 29.25/29.30 cnf('1.4',plain,[-(4 ^ []), -(xsd_integer(3 ^ []))],extension(8)).
% 29.25/29.30 cnf('1.4.1',plain,[xsd_integer(3 ^ []), -(xsd_integer(3 ^ [])), 3 ^ [] = 3 ^ []],extension(17,bind([[_11187, _11236], [3 ^ [], 3 ^ []]]))).
% 29.25/29.30 cnf('1.4.1.1',plain,[xsd_integer(3 ^ []), -(xsd_integer(3 ^ [])), 3 ^ [] = 3 ^ []],extension(17,bind([[_11187, _11236], [3 ^ [], 3 ^ []]]))).
% 29.25/29.30 cnf('1.4.1.1.1',plain,[xsd_integer(3 ^ []), -(xsd_integer(3 ^ [])), 3 ^ [] = 3 ^ []],extension(17,bind([[_11187, _11236], [3 ^ [], 3 ^ []]]))).
% 29.25/29.30 cnf('1.4.1.1.1.1',plain,[xsd_integer(3 ^ []), -(xsd_integer(3 ^ [])), 3 ^ [] = 3 ^ []],extension(17,bind([[_11187, _11236], [3 ^ [], 3 ^ []]]))).
% 29.25/29.30 cnf('1.4.1.1.1.1.1',plain,[xsd_integer(3 ^ []), xsd_string(3 ^ [])],extension(21,bind([[_14858], [3 ^ []]]))).
% 29.25/29.30 cnf('1.4.1.1.1.1.1.1',plain,[-(xsd_string(3 ^ [])), -(4 ^ [])],extension(9)).
% 29.25/29.30 cnf('1.4.1.1.1.1.1.1.1',plain,[4 ^ []],reduction('1')).
% 29.25/29.30 cnf('1.4.1.1.1.1.2',plain,[-(3 ^ [] = 3 ^ [])],extension(11,bind([[_8668], [3 ^ []]]))).
% 29.25/29.30 cnf('1.4.1.1.1.2',plain,[-(3 ^ [] = 3 ^ [])],extension(11,bind([[_8668], [3 ^ []]]))).
% 29.25/29.30 cnf('1.4.1.1.2',plain,[-(3 ^ [] = 3 ^ [])],extension(11,bind([[_8668], [3 ^ []]]))).
% 29.25/29.30 cnf('1.4.1.2',plain,[-(3 ^ [] = 3 ^ [])],extension(11,bind([[_8668], [3 ^ []]]))).
% 29.25/29.30 cnf('1.5',plain,[-(8 ^ []), -(requalityOnA(6 ^ [], 7 ^ []))],extension(5)).
% 29.25/29.30 cnf('1.5.1',plain,[requalityOnA(6 ^ [], 7 ^ []), -(cA(7 ^ []))],extension(26,bind([[_15865, _15909], [6 ^ [], 7 ^ []]]))).
% 29.25/29.30 cnf('1.5.1.1',plain,[cA(7 ^ []), -(7 ^ [] = ib), -(7 ^ [] = ia)],extension(23,bind([[_15086], [7 ^ []]]))).
% 29.25/29.30 cnf('1.5.1.1.1',plain,[7 ^ [] = ib, -(7 ^ [] = 6 ^ []), ib = 6 ^ []],extension(13,bind([[_9100, _9156, _9211], [7 ^ [], ib, 6 ^ []]]))).
% 29.25/29.30 cnf('1.5.1.1.1.1',plain,[7 ^ [] = 6 ^ [], -(cA(6 ^ [])), cA(7 ^ [])],extension(14,bind([[_9625, _9576], [6 ^ [], 7 ^ []]]))).
% 29.25/29.30 cnf('1.5.1.1.1.1.1',plain,[cA(6 ^ []), -(6 ^ [] = ib), -(6 ^ [] = ia)],extension(23,bind([[_15086], [6 ^ []]]))).
% 29.25/29.30 cnf('1.5.1.1.1.1.1.1',plain,[6 ^ [] = ib, -(8 ^ [])],extension(3)).
% 29.25/29.30 cnf('1.5.1.1.1.1.1.1.1',plain,[8 ^ []],reduction('1')).
% 29.25/29.30 cnf('1.5.1.1.1.1.1.2',plain,[6 ^ [] = ia, -(8 ^ [])],extension(4)).
% 29.25/29.30 cnf('1.5.1.1.1.1.1.2.1',plain,[8 ^ []],reduction('1')).
% 29.25/29.30 cnf('1.5.1.1.1.1.2',plain,[-(cA(7 ^ []))],reduction('1.5.1')).
% 29.25/29.30 cnf('1.5.1.1.1.2',plain,[-(ib = 6 ^ []), requalityOnA(ib, ib), requalityOnA(6 ^ [], ib)],extension(27,bind([[_15454, _15509, _15398], [ib, 6 ^ [], ib]]))).
% 29.25/29.30 cnf('1.5.1.1.1.2.1',plain,[-(requalityOnA(ib, ib))],extension(25)).
% 29.25/29.30 cnf('1.5.1.1.1.2.2',plain,[-(requalityOnA(6 ^ [], ib)), 7 ^ [] = ib, requalityOnA(6 ^ [], 7 ^ [])],extension(18,bind([[_13519, _13574, _13463], [ib, 6 ^ [], 7 ^ []]]))).
% 29.25/29.30 cnf('1.5.1.1.1.2.2.1',plain,[-(7 ^ [] = ib)],reduction('1.5.1.1')).
% 29.25/29.30 cnf('1.5.1.1.1.2.2.2',plain,[-(requalityOnA(6 ^ [], 7 ^ []))],reduction('1.5')).
% 29.25/29.30 cnf('1.5.1.1.2',plain,[7 ^ [] = ia, -(7 ^ [] = 6 ^ []), ia = 6 ^ []],extension(13,bind([[_9100, _9156, _9211], [7 ^ [], ia, 6 ^ []]]))).
% 29.25/29.30 cnf('1.5.1.1.2.1',plain,[7 ^ [] = 6 ^ [], -(cA(6 ^ [])), cA(7 ^ [])],extension(14,bind([[_9625, _9576], [6 ^ [], 7 ^ []]]))).
% 29.25/29.30 cnf('1.5.1.1.2.1.1',plain,[cA(6 ^ []), -(6 ^ [] = ib), -(6 ^ [] = ia)],extension(23,bind([[_15086], [6 ^ []]]))).
% 29.25/29.30 cnf('1.5.1.1.2.1.1.1',plain,[6 ^ [] = ib, -(8 ^ [])],extension(3)).
% 29.25/29.30 cnf('1.5.1.1.2.1.1.1.1',plain,[8 ^ []],reduction('1')).
% 29.25/29.30 cnf('1.5.1.1.2.1.1.2',plain,[6 ^ [] = ia, -(8 ^ [])],extension(4)).
% 29.25/29.30 cnf('1.5.1.1.2.1.1.2.1',plain,[8 ^ []],reduction('1')).
% 29.25/29.30 cnf('1.5.1.1.2.1.2',plain,[-(cA(7 ^ []))],reduction('1.5.1')).
% 29.25/29.30 cnf('1.5.1.1.2.2',plain,[-(ia = 6 ^ []), requalityOnA(ia, ia), requalityOnA(6 ^ [], ia)],extension(27,bind([[_15454, _15509, _15398], [ia, 6 ^ [], ia]]))).
% 29.25/29.30 cnf('1.5.1.1.2.2.1',plain,[-(requalityOnA(ia, ia))],extension(24)).
% 29.25/29.30 cnf('1.5.1.1.2.2.2',plain,[-(requalityOnA(6 ^ [], ia)), 7 ^ [] = ia, requalityOnA(6 ^ [], 7 ^ [])],extension(18,bind([[_13519, _13574, _13463], [ia, 6 ^ [], 7 ^ []]]))).
% 29.25/29.30 cnf('1.5.1.1.2.2.2.1',plain,[-(7 ^ [] = ia)],reduction('1.5.1.1')).
% 29.25/29.30 cnf('1.5.1.1.2.2.2.2',plain,[-(requalityOnA(6 ^ [], 7 ^ []))],reduction('1.5')).
% 29.25/29.30 cnf('1.6',plain,[-(11 ^ []), -(requalityOnA(9 ^ [], 10 ^ []))],extension(2)).
% 29.25/29.30 cnf('1.6.1',plain,[requalityOnA(9 ^ [], 10 ^ []), -(cA(10 ^ []))],extension(26,bind([[_15865, _15909], [9 ^ [], 10 ^ []]]))).
% 29.25/29.30 cnf('1.6.1.1',plain,[cA(10 ^ []), -(10 ^ [] = ib), -(10 ^ [] = ia)],extension(23,bind([[_15086], [10 ^ []]]))).
% 29.25/29.30 cnf('1.6.1.1.1',plain,[10 ^ [] = ib, -(10 ^ [] = 9 ^ []), ib = 9 ^ []],extension(13,bind([[_9100, _9156, _9211], [10 ^ [], ib, 9 ^ []]]))).
% 29.25/29.30 cnf('1.6.1.1.1.1',plain,[10 ^ [] = 9 ^ [], -(9 ^ [] = 10 ^ [])],extension(12,bind([[_8866, _8821], [9 ^ [], 10 ^ []]]))).
% 29.25/29.30 cnf('1.6.1.1.1.1.1',plain,[9 ^ [] = 10 ^ [], -(requalityOnA(10 ^ [], 9 ^ [])), requalityOnA(9 ^ [], 10 ^ []), 10 ^ [] = 9 ^ []],extension(16,bind([[_10630, _10563, _10696, _10761], [10 ^ [], 9 ^ [], 10 ^ [], 9 ^ []]]))).
% 29.25/29.30 cnf('1.6.1.1.1.1.1.1',plain,[requalityOnA(10 ^ [], 9 ^ []), -(11 ^ [])],extension(1)).
% 29.25/29.30 cnf('1.6.1.1.1.1.1.1.1',plain,[11 ^ []],reduction('1')).
% 29.25/29.30 cnf('1.6.1.1.1.1.1.2',plain,[-(requalityOnA(9 ^ [], 10 ^ []))],reduction('1.6')).
% 29.25/29.30 cnf('1.6.1.1.1.1.1.3',plain,[-(10 ^ [] = 9 ^ [])],reduction('1.6.1.1.1')).
% 29.25/29.30 cnf('1.6.1.1.1.2',plain,[-(ib = 9 ^ []), requalityOnA(ib, ib), requalityOnA(9 ^ [], ib)],extension(27,bind([[_15454, _15509, _15398], [ib, 9 ^ [], ib]]))).
% 29.25/29.30 cnf('1.6.1.1.1.2.1',plain,[-(requalityOnA(ib, ib))],extension(25)).
% 29.25/29.30 cnf('1.6.1.1.1.2.2',plain,[-(requalityOnA(9 ^ [], ib)), 10 ^ [] = ib, requalityOnA(9 ^ [], 10 ^ [])],extension(18,bind([[_13519, _13574, _13463], [ib, 9 ^ [], 10 ^ []]]))).
% 29.25/29.30 cnf('1.6.1.1.1.2.2.1',plain,[-(10 ^ [] = ib)],reduction('1.6.1.1')).
% 29.25/29.30 cnf('1.6.1.1.1.2.2.2',plain,[-(requalityOnA(9 ^ [], 10 ^ []))],reduction('1.6')).
% 29.25/29.30 cnf('1.6.1.1.2',plain,[10 ^ [] = ia, -(10 ^ [] = 9 ^ []), ia = 9 ^ []],extension(13,bind([[_9100, _9156, _9211], [10 ^ [], ia, 9 ^ []]]))).
% 29.25/29.30 cnf('1.6.1.1.2.1',plain,[10 ^ [] = 9 ^ [], -(9 ^ [] = 10 ^ [])],extension(12,bind([[_8866, _8821], [9 ^ [], 10 ^ []]]))).
% 29.25/29.30 cnf('1.6.1.1.2.1.1',plain,[9 ^ [] = 10 ^ [], -(requalityOnA(10 ^ [], 9 ^ [])), requalityOnA(9 ^ [], 10 ^ []), 10 ^ [] = 9 ^ []],extension(16,bind([[_10630, _10563, _10696, _10761], [10 ^ [], 9 ^ [], 10 ^ [], 9 ^ []]]))).
% 29.25/29.30 cnf('1.6.1.1.2.1.1.1',plain,[requalityOnA(10 ^ [], 9 ^ []), -(11 ^ [])],extension(1)).
% 29.25/29.30 cnf('1.6.1.1.2.1.1.1.1',plain,[11 ^ []],reduction('1')).
% 29.25/29.30 cnf('1.6.1.1.2.1.1.2',plain,[-(requalityOnA(9 ^ [], 10 ^ []))],reduction('1.6')).
% 29.25/29.30 cnf('1.6.1.1.2.1.1.3',plain,[-(10 ^ [] = 9 ^ [])],reduction('1.6.1.1.2')).
% 29.25/29.30 cnf('1.6.1.1.2.2',plain,[-(ia = 9 ^ []), requalityOnA(ia, ia), requalityOnA(9 ^ [], ia)],extension(27,bind([[_15454, _15509, _15398], [ia, 9 ^ [], ia]]))).
% 29.25/29.30 cnf('1.6.1.1.2.2.1',plain,[-(requalityOnA(ia, ia))],extension(24)).
% 29.25/29.30 cnf('1.6.1.1.2.2.2',plain,[-(requalityOnA(9 ^ [], ia)), 10 ^ [] = ia, requalityOnA(9 ^ [], 10 ^ [])],extension(18,bind([[_13519, _13574, _13463], [ia, 9 ^ [], 10 ^ []]]))).
% 29.25/29.30 cnf('1.6.1.1.2.2.2.1',plain,[-(10 ^ [] = ia)],reduction('1.6.1.1')).
% 29.25/29.30 cnf('1.6.1.1.2.2.2.2',plain,[-(requalityOnA(9 ^ [], 10 ^ []))],reduction('1.6')).
% 29.25/29.30 cnf('1.7',plain,[-(cowlThing(ia))],extension(19,bind([[_14630], [ia]]))).
% 29.25/29.30 cnf('1.8',plain,[-(requalityOnA(ia, ia)), requalityOnA(ia, ia), ia = ia, ia = ia],extension(16,bind([[_10563, _10630, _10696, _10761], [ia, ia, ia, ia]]))).
% 29.25/29.30 cnf('1.8.1',plain,[-(requalityOnA(ia, ia)), requalityOnA(ia, ia), ia = ia, ia = ia],extension(16,bind([[_10563, _10630, _10696, _10761], [ia, ia, ia, ia]]))).
% 29.25/29.30 cnf('1.8.1.1',plain,[-(requalityOnA(ia, ia)), requalityOnA(ia, ia), ia = ia, ia = ia],extension(16,bind([[_10563, _10630, _10696, _10761], [ia, ia, ia, ia]]))).
% 29.25/29.30 cnf('1.8.1.1.1',plain,[-(requalityOnA(ia, ia)), requalityOnA(ia, ia), ia = ia, ia = ia],extension(16,bind([[_10563, _10630, _10696, _10761], [ia, ia, ia, ia]]))).
% 29.25/29.30 cnf('1.8.1.1.1.1',plain,[-(requalityOnA(ia, ia)), requalityOnA(ia, ia), ia = ia, ia = ia],extension(16,bind([[_10563, _10630, _10696, _10761], [ia, ia, ia, ia]]))).
% 29.25/29.30 cnf('1.8.1.1.1.1.1',plain,[-(requalityOnA(ia, ia))],extension(24)).
% 29.25/29.30 cnf('1.8.1.1.1.1.2',plain,[-(ia = ia)],extension(11,bind([[_8668], [ia]]))).
% 29.25/29.30 cnf('1.8.1.1.1.1.3',plain,[-(ia = ia)],extension(11,bind([[_8668], [ia]]))).
% 29.25/29.30 cnf('1.8.1.1.1.2',plain,[-(ia = ia)],extension(11,bind([[_8668], [ia]]))).
% 29.25/29.30 cnf('1.8.1.1.1.3',plain,[-(ia = ia)],extension(11,bind([[_8668], [ia]]))).
% 29.25/29.30 cnf('1.8.1.1.2',plain,[-(ia = ia)],extension(11,bind([[_8668], [ia]]))).
% 29.25/29.30 cnf('1.8.1.1.3',plain,[-(ia = ia)],extension(11,bind([[_8668], [ia]]))).
% 29.25/29.30 cnf('1.8.1.2',plain,[-(ia = ia)],extension(11,bind([[_8668], [ia]]))).
% 29.25/29.30 cnf('1.8.1.3',plain,[-(ia = ia)],extension(11,bind([[_8668], [ia]]))).
% 29.25/29.30 cnf('1.8.2',plain,[-(ia = ia)],extension(11,bind([[_8668], [ia]]))).
% 29.25/29.30 cnf('1.8.3',plain,[-(ia = ia)],extension(11,bind([[_8668], [ia]]))).
% 29.25/29.30 cnf('1.9',plain,[-(cowlThing(ib))],extension(19,bind([[_14630], [ib]]))).
% 29.25/29.30 cnf('1.10',plain,[-(cowlThing(ic))],extension(19,bind([[_14630], [ic]]))).
% 29.25/29.30 %-----------------------------------------------------
% 29.25/29.30
% 29.25/29.30 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------