%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : KRS155+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n019.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:51 EDT 2022
% Result : Theorem 2.45s 3.47s
% Output : Proof 2.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KRS155+1 : TPTP v8.1.0. Released v3.1.0.
% 0.07/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n019.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 : Tue Jun 7 14:53:55 EDT 2022
% 0.13/0.34 % CPUTime :
% 2.45/3.47 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.45/3.47 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.51/3.48
% 2.51/3.48 %-----------------------------------------------------
% 2.51/3.48 fof(the_axiom, conjecture, ! [_113132] : (cowlThing(_113132) & ~ cowlNothing(_113132)) & ! [_113132] : (xsd_string(_113132) <=> ~ xsd_integer(_113132)) & cC20(iV8467) & cC4(iV8467) & cC8(iV8467) & cC82(iV8467) & cC62(iV8467) & cC14(iV8467) & cC34(iV8467) & cC10(iV8467) & cowlThing(iV8467) & cC48(iV8467) & cowlThing(iV8471) & cC80(iV8471) & cC58(iV8472) & cC60(iV8472) & cowlThing(iV8472), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', the_axiom)).
% 2.51/3.48 fof(axiom_0, axiom, ! [_113697] : (cowlThing(_113697) & ~ cowlNothing(_113697)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_0)).
% 2.51/3.48 fof(axiom_1, axiom, ! [_113837] : (xsd_string(_113837) <=> ~ xsd_integer(_113837)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_1)).
% 2.51/3.48 fof(axiom_2, axiom, ! [_113979] : (cC10(_113979) <=> cC4(_113979) & cC8(_113979)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 2.51/3.48 fof(axiom_5, axiom, ! [_114128] : (cC14(_114128) <=> ? [_114143] : (rR1(_114128, _114143) & cTOP(_114143))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_5)).
% 2.51/3.48 fof(axiom_13, axiom, ! [_114323] : (cC20(_114323) <=> ? [_114338] : (rR1(_114323, _114338) & cC2xcomp(_114338))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_13)).
% 2.51/3.48 fof(axiom_16, axiom, ! [_114530] : (cC22(_114530) <=> ? [_114545] : (rR1(_114530, _114545) & cC2xcomp(_114545))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_16)).
% 2.51/3.48 fof(axiom_25, axiom, ! [_114753] : (cC32(_114753) <=> ? [_114768] : (rR1(_114753, _114768) & cC2(_114768))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_25)).
% 2.51/3.48 fof(axiom_29, axiom, ! [_114964] : (cC34(_114964) <=> ? [_114979] : (rR1(_114964, _114979) & cC32xcomp(_114979))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_29)).
% 2.51/3.48 fof(axiom_35, axiom, ! [_115157] : (cC4(_115157) <=> ? [_115172] : (rR1(_115157, _115172) & cC2xcomp(_115172))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_35)).
% 2.51/3.48 fof(axiom_44, axiom, ! [_115358] : (cC48(_115358) <=> ? [_115373] : (rR1(_115358, _115373) & cC2xcomp(_115373))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_44)).
% 2.51/3.48 fof(axiom_57, axiom, ! [_115567] : (cC58(_115567) <=> ? [_115582] : (rR1(_115567, _115582) & cC2(_115582))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_57)).
% 2.51/3.48 fof(axiom_61, axiom, ! [_115755] : (cC60(_115755) <=> cC2xcomp(_115755) & cC58(_115755)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_61)).
% 2.51/3.48 fof(axiom_62, axiom, ! [_115899] : (cC62(_115899) <=> ? [_115914] : (rR1(_115899, _115914) & cC60(_115914))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_62)).
% 2.51/3.48 fof(axiom_79, axiom, ! [_116120] : (cC8(_116120) <=> ? [_116135] : (rR1(_116120, _116135) & cC6xcomp(_116135))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_79)).
% 2.51/3.48 fof(axiom_80, axiom, ! [_116301] : (cC80(_116301) <=> cC78xcomp(_116301) & cC2xcomp(_116301)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_80)).
% 2.51/3.48 fof(axiom_82, axiom, ! [_116447] : (cC82(_116447) <=> ? [_116462] : (rR1(_116447, _116462) & cC80(_116462))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_82)).
% 2.51/3.48 fof(axiom_103, axiom, rR1(iV8467, iV8471), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_103)).
% 2.51/3.48 fof(axiom_104, axiom, rR1(iV8467, iV8470), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_104)).
% 2.51/3.48 fof(axiom_105, axiom, rR1(iV8467, iV8469), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_105)).
% 2.51/3.48 fof(axiom_106, axiom, rR1(iV8467, iV8474), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_106)).
% 2.51/3.48 fof(axiom_110, axiom, rR1(iV8467, iV8472), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_110)).
% 2.51/3.48 fof(axiom_113, axiom, cC6xcomp(iV8469), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_113)).
% 2.51/3.48 fof(axiom_116, axiom, cTOP(iV8470), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_116)).
% 2.51/3.48 fof(axiom_118, axiom, cC78xcomp(iV8471), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_118)).
% 2.51/3.48 fof(axiom_119, axiom, cC2xcomp(iV8471), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_119)).
% 2.51/3.48 fof(axiom_122, axiom, cC2xcomp(iV8472), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_122)).
% 2.51/3.48 fof(axiom_124, axiom, rR1(iV8472, iV8476), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_124)).
% 2.51/3.48 fof(axiom_127, axiom, cC32xcomp(iV8474), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_127)).
% 2.51/3.48 fof(axiom_132, axiom, cC2(iV8476), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_132)).
% 2.51/3.48
% 2.51/3.48 cnf(1, plain, [-(83 ^ []), xsd_string(81 ^ [])], clausify(the_axiom)).
% 2.51/3.48 cnf(2, plain, [-(83 ^ []), xsd_integer(81 ^ [])], clausify(the_axiom)).
% 2.51/3.48 cnf(3, plain, [-(82 ^ []), -(xsd_integer(81 ^ []))], clausify(the_axiom)).
% 2.51/3.48 cnf(4, plain, [-(82 ^ []), -(xsd_string(81 ^ []))], clausify(the_axiom)).
% 2.51/3.48 cnf(5, plain, [-(cowlNothing(80 ^ [])), cowlThing(80 ^ []), 83 ^ [], 82 ^ [], cC20(iV8467), cC4(iV8467), cC8(iV8467), cC82(iV8467), cC62(iV8467), cC14(iV8467), cC34(iV8467), cC10(iV8467), cowlThing(iV8467), cC48(iV8467), cowlThing(iV8471), cC80(iV8471), cC58(iV8472), cC60(iV8472), cowlThing(iV8472)], clausify(the_axiom)).
% 2.51/3.48 cnf(6, plain, [-(cowlThing(_24539))], clausify(axiom_0)).
% 2.51/3.48 cnf(7, plain, [cowlNothing(_24539)], clausify(axiom_0)).
% 2.51/3.48 cnf(8, plain, [xsd_string(_24767), xsd_integer(_24767)], clausify(axiom_1)).
% 2.51/3.48 cnf(9, plain, [-(xsd_string(_24767)), -(xsd_integer(_24767))], clausify(axiom_1)).
% 2.51/3.48 cnf(10, plain, [-(cC10(_24995)), cC4(_24995), cC8(_24995)], clausify(axiom_2)).
% 2.51/3.48 cnf(11, plain, [-(cC14(_25910)), rR1(_25910, _25998), cTOP(_25998)], clausify(axiom_5)).
% 2.51/3.48 cnf(12, plain, [cC20(_28321), -(rR1(_28321, 10 ^ [_28321]))], clausify(axiom_13)).
% 2.51/3.48 cnf(13, plain, [cC20(_28321), -(cC2xcomp(10 ^ [_28321]))], clausify(axiom_13)).
% 2.51/3.48 cnf(14, plain, [-(cC20(_28321)), rR1(_28321, _28409), cC2xcomp(_28409)], clausify(axiom_13)).
% 2.51/3.48 cnf(15, plain, [cC22(_29251), -(rR1(_29251, 13 ^ [_29251]))], clausify(axiom_16)).
% 2.51/3.48 cnf(16, plain, [cC22(_29251), -(cC2xcomp(13 ^ [_29251]))], clausify(axiom_16)).
% 2.51/3.48 cnf(17, plain, [-(cC22(_29251)), rR1(_29251, _29339), cC2xcomp(_29339)], clausify(axiom_16)).
% 2.51/3.48 cnf(18, plain, [cC32(_31993), -(rR1(_31993, 20 ^ [_31993]))], clausify(axiom_25)).
% 2.51/3.48 cnf(19, plain, [cC32(_31993), -(cC2(20 ^ [_31993]))], clausify(axiom_25)).
% 2.51/3.48 cnf(20, plain, [-(cC32(_31993)), rR1(_31993, _32081), cC2(_32081)], clausify(axiom_25)).
% 2.51/3.48 cnf(21, plain, [-(cC34(_33206)), rR1(_33206, _33294), cC32xcomp(_33294)], clausify(axiom_29)).
% 2.51/3.48 cnf(22, plain, [-(cC4(_35129)), rR1(_35129, _35217), cC2xcomp(_35217)], clausify(axiom_35)).
% 2.51/3.48 cnf(23, plain, [-(cC48(_37871)), rR1(_37871, _37959), cC2xcomp(_37959)], clausify(axiom_44)).
% 2.51/3.48 cnf(24, plain, [-(cC58(_41781)), rR1(_41781, _41869), cC2(_41869)], clausify(axiom_57)).
% 2.51/3.48 cnf(25, plain, [-(cC60(_43057)), cC2xcomp(_43057), cC58(_43057)], clausify(axiom_61)).
% 2.51/3.48 cnf(26, plain, [-(cC62(_43325)), rR1(_43325, _43413), cC60(_43413)], clausify(axiom_62)).
% 2.51/3.48 cnf(27, plain, [-(cC8(_48541)), rR1(_48541, _48629), cC6xcomp(_48629)], clausify(axiom_79)).
% 2.51/3.48 cnf(28, plain, [-(cC80(_48887)), cC78xcomp(_48887), cC2xcomp(_48887)], clausify(axiom_80)).
% 2.51/3.48 cnf(29, plain, [-(cC82(_49456)), rR1(_49456, _49544), cC80(_49544)], clausify(axiom_82)).
% 2.51/3.48 cnf(30, plain, [-(rR1(iV8467, iV8471))], clausify(axiom_103)).
% 2.51/3.48 cnf(31, plain, [-(rR1(iV8467, iV8470))], clausify(axiom_104)).
% 2.51/3.48 cnf(32, plain, [-(rR1(iV8467, iV8469))], clausify(axiom_105)).
% 2.51/3.48 cnf(33, plain, [-(rR1(iV8467, iV8474))], clausify(axiom_106)).
% 2.51/3.48 cnf(34, plain, [-(rR1(iV8467, iV8472))], clausify(axiom_110)).
% 2.51/3.48 cnf(35, plain, [-(cC6xcomp(iV8469))], clausify(axiom_113)).
% 2.51/3.48 cnf(36, plain, [-(cTOP(iV8470))], clausify(axiom_116)).
% 2.51/3.48 cnf(37, plain, [-(cC78xcomp(iV8471))], clausify(axiom_118)).
% 2.51/3.48 cnf(38, plain, [-(cC2xcomp(iV8471))], clausify(axiom_119)).
% 2.51/3.48 cnf(39, plain, [-(cC2xcomp(iV8472))], clausify(axiom_122)).
% 2.51/3.48 cnf(40, plain, [-(rR1(iV8472, iV8476))], clausify(axiom_124)).
% 2.51/3.48 cnf(41, plain, [-(cC32xcomp(iV8474))], clausify(axiom_127)).
% 2.51/3.48 cnf(42, plain, [-(cC2(iV8476))], clausify(axiom_132)).
% 2.51/3.48
% 2.51/3.48 cnf('1',plain,[cowlNothing(80 ^ [])],start(7,bind([[_24539], [80 ^ []]]))).
% 2.51/3.48 cnf('1.1',plain,[-(cowlNothing(80 ^ [])), cowlThing(80 ^ []), 83 ^ [], 82 ^ [], cC20(iV8467), cC4(iV8467), cC8(iV8467), cC82(iV8467), cC62(iV8467), cC14(iV8467), cC34(iV8467), cC10(iV8467), cowlThing(iV8467), cC48(iV8467), cowlThing(iV8471), cC80(iV8471), cC58(iV8472), cC60(iV8472), cowlThing(iV8472)],extension(5)).
% 2.51/3.48 cnf('1.1.1',plain,[-(cowlThing(80 ^ []))],extension(6,bind([[_24539], [80 ^ []]]))).
% 2.51/3.48 cnf('1.1.2',plain,[-(83 ^ []), xsd_string(81 ^ [])],extension(1)).
% 2.51/3.48 cnf('1.1.2.1',plain,[-(xsd_string(81 ^ [])), -(xsd_integer(81 ^ []))],extension(9,bind([[_24767], [81 ^ []]]))).
% 2.51/3.48 cnf('1.1.2.1.1',plain,[xsd_integer(81 ^ []), -(83 ^ [])],extension(2)).
% 2.51/3.48 cnf('1.1.2.1.1.1',plain,[83 ^ []],reduction('1.1')).
% 2.51/3.48 cnf('1.1.3',plain,[-(82 ^ []), -(xsd_integer(81 ^ []))],extension(3)).
% 2.51/3.48 cnf('1.1.3.1',plain,[xsd_integer(81 ^ []), xsd_string(81 ^ [])],extension(8,bind([[_24767], [81 ^ []]]))).
% 2.51/3.48 cnf('1.1.3.1.1',plain,[-(xsd_string(81 ^ [])), -(82 ^ [])],extension(4)).
% 2.51/3.48 cnf('1.1.3.1.1.1',plain,[82 ^ []],reduction('1.1')).
% 2.51/3.48 cnf('1.1.4',plain,[-(cC20(iV8467)), rR1(iV8467, 13 ^ [iV8467]), cC2xcomp(13 ^ [iV8467])],extension(14,bind([[_28321, _28409], [iV8467, 13 ^ [iV8467]]]))).
% 2.51/3.48 cnf('1.1.4.1',plain,[-(rR1(iV8467, 13 ^ [iV8467])), cC22(iV8467)],extension(15,bind([[_29251], [iV8467]]))).
% 2.51/3.48 cnf('1.1.4.1.1',plain,[-(cC22(iV8467)), rR1(iV8467, iV8471), cC2xcomp(iV8471)],extension(17,bind([[_29251, _29339], [iV8467, iV8471]]))).
% 2.51/3.48 cnf('1.1.4.1.1.1',plain,[-(rR1(iV8467, iV8471))],extension(30)).
% 2.51/3.48 cnf('1.1.4.1.1.2',plain,[-(cC2xcomp(iV8471))],extension(38)).
% 2.51/3.48 cnf('1.1.4.2',plain,[-(cC2xcomp(13 ^ [iV8467])), cC22(iV8467)],extension(16,bind([[_29251], [iV8467]]))).
% 2.51/3.48 cnf('1.1.4.2.1',plain,[-(cC22(iV8467)), rR1(iV8467, iV8471), cC2xcomp(iV8471)],extension(17,bind([[_29251, _29339], [iV8467, iV8471]]))).
% 2.51/3.48 cnf('1.1.4.2.1.1',plain,[-(rR1(iV8467, iV8471))],extension(30)).
% 2.51/3.48 cnf('1.1.4.2.1.2',plain,[-(cC2xcomp(iV8471))],extension(38)).
% 2.51/3.48 cnf('1.1.5',plain,[-(cC4(iV8467)), rR1(iV8467, 10 ^ [iV8467]), cC2xcomp(10 ^ [iV8467])],extension(22,bind([[_35129, _35217], [iV8467, 10 ^ [iV8467]]]))).
% 2.51/3.48 cnf('1.1.5.1',plain,[-(rR1(iV8467, 10 ^ [iV8467])), cC20(iV8467)],extension(12,bind([[_28321], [iV8467]]))).
% 2.51/3.48 cnf('1.1.5.1.1',plain,[-(cC20(iV8467))],lemmata('1.1')).
% 2.51/3.48 cnf('1.1.5.2',plain,[-(cC2xcomp(10 ^ [iV8467])), cC20(iV8467)],extension(13,bind([[_28321], [iV8467]]))).
% 2.51/3.48 cnf('1.1.5.2.1',plain,[-(cC20(iV8467))],lemmata('1.1')).
% 2.51/3.48 cnf('1.1.6',plain,[-(cC8(iV8467)), rR1(iV8467, iV8469), cC6xcomp(iV8469)],extension(27,bind([[_48541, _48629], [iV8467, iV8469]]))).
% 2.51/3.48 cnf('1.1.6.1',plain,[-(rR1(iV8467, iV8469))],extension(32)).
% 2.51/3.48 cnf('1.1.6.2',plain,[-(cC6xcomp(iV8469))],extension(35)).
% 2.51/3.48 cnf('1.1.7',plain,[-(cC82(iV8467)), rR1(iV8467, iV8471), cC80(iV8471)],extension(29,bind([[_49456, _49544], [iV8467, iV8471]]))).
% 2.51/3.48 cnf('1.1.7.1',plain,[-(rR1(iV8467, iV8471))],extension(30)).
% 2.51/3.48 cnf('1.1.7.2',plain,[-(cC80(iV8471)), cC78xcomp(iV8471), cC2xcomp(iV8471)],extension(28,bind([[_48887], [iV8471]]))).
% 2.51/3.48 cnf('1.1.7.2.1',plain,[-(cC78xcomp(iV8471))],extension(37)).
% 2.51/3.48 cnf('1.1.7.2.2',plain,[-(cC2xcomp(iV8471))],extension(38)).
% 2.51/3.48 cnf('1.1.8',plain,[-(cC62(iV8467)), rR1(iV8467, iV8472), cC60(iV8472)],extension(26,bind([[_43325, _43413], [iV8467, iV8472]]))).
% 2.51/3.48 cnf('1.1.8.1',plain,[-(rR1(iV8467, iV8472))],extension(34)).
% 2.51/3.48 cnf('1.1.8.2',plain,[-(cC60(iV8472)), cC2xcomp(iV8472), cC58(iV8472)],extension(25,bind([[_43057], [iV8472]]))).
% 2.51/3.48 cnf('1.1.8.2.1',plain,[-(cC2xcomp(iV8472))],extension(39)).
% 2.51/3.48 cnf('1.1.8.2.2',plain,[-(cC58(iV8472)), rR1(iV8472, iV8476), cC2(iV8476)],extension(24,bind([[_41781, _41869], [iV8472, iV8476]]))).
% 2.51/3.48 cnf('1.1.8.2.2.1',plain,[-(rR1(iV8472, iV8476))],extension(40)).
% 2.51/3.48 cnf('1.1.8.2.2.2',plain,[-(cC2(iV8476))],extension(42)).
% 2.51/3.48 cnf('1.1.9',plain,[-(cC14(iV8467)), rR1(iV8467, iV8470), cTOP(iV8470)],extension(11,bind([[_25910, _25998], [iV8467, iV8470]]))).
% 2.51/3.48 cnf('1.1.9.1',plain,[-(rR1(iV8467, iV8470))],extension(31)).
% 2.51/3.48 cnf('1.1.9.2',plain,[-(cTOP(iV8470))],extension(36)).
% 2.51/3.48 cnf('1.1.10',plain,[-(cC34(iV8467)), rR1(iV8467, iV8474), cC32xcomp(iV8474)],extension(21,bind([[_33206, _33294], [iV8467, iV8474]]))).
% 2.51/3.48 cnf('1.1.10.1',plain,[-(rR1(iV8467, iV8474))],extension(33)).
% 2.51/3.48 cnf('1.1.10.2',plain,[-(cC32xcomp(iV8474))],extension(41)).
% 2.51/3.48 cnf('1.1.11',plain,[-(cC10(iV8467)), cC4(iV8467), cC8(iV8467)],extension(10,bind([[_24995], [iV8467]]))).
% 2.51/3.48 cnf('1.1.11.1',plain,[-(cC4(iV8467))],lemmata('1.1')).
% 2.51/3.48 cnf('1.1.11.2',plain,[-(cC8(iV8467))],lemmata('1.1')).
% 2.51/3.48 cnf('1.1.12',plain,[-(cowlThing(iV8467))],extension(6,bind([[_24539], [iV8467]]))).
% 2.51/3.48 cnf('1.1.13',plain,[-(cC48(iV8467)), rR1(iV8467, 10 ^ [iV8467]), cC2xcomp(10 ^ [iV8467])],extension(23,bind([[_37871, _37959], [iV8467, 10 ^ [iV8467]]]))).
% 2.51/3.48 cnf('1.1.13.1',plain,[-(rR1(iV8467, 10 ^ [iV8467])), cC20(iV8467)],extension(12,bind([[_28321], [iV8467]]))).
% 2.51/3.48 cnf('1.1.13.1.1',plain,[-(cC20(iV8467))],lemmata('1.1')).
% 2.51/3.48 cnf('1.1.13.2',plain,[-(cC2xcomp(10 ^ [iV8467])), cC20(iV8467)],extension(13,bind([[_28321], [iV8467]]))).
% 2.51/3.48 cnf('1.1.13.2.1',plain,[-(cC20(iV8467))],lemmata('1.1')).
% 2.51/3.48 cnf('1.1.14',plain,[-(cowlThing(iV8471))],extension(6,bind([[_24539], [iV8471]]))).
% 2.51/3.48 cnf('1.1.15',plain,[-(cC80(iV8471)), cC78xcomp(iV8471), cC2xcomp(iV8471)],extension(28,bind([[_48887], [iV8471]]))).
% 2.51/3.48 cnf('1.1.15.1',plain,[-(cC78xcomp(iV8471))],extension(37)).
% 2.51/3.48 cnf('1.1.15.2',plain,[-(cC2xcomp(iV8471))],extension(38)).
% 2.51/3.48 cnf('1.1.16',plain,[-(cC58(iV8472)), rR1(iV8472, 20 ^ [iV8472]), cC2(20 ^ [iV8472])],extension(24,bind([[_41781, _41869], [iV8472, 20 ^ [iV8472]]]))).
% 2.51/3.48 cnf('1.1.16.1',plain,[-(rR1(iV8472, 20 ^ [iV8472])), cC32(iV8472)],extension(18,bind([[_31993], [iV8472]]))).
% 2.51/3.48 cnf('1.1.16.1.1',plain,[-(cC32(iV8472)), rR1(iV8472, iV8476), cC2(iV8476)],extension(20,bind([[_31993, _32081], [iV8472, iV8476]]))).
% 2.51/3.48 cnf('1.1.16.1.1.1',plain,[-(rR1(iV8472, iV8476))],extension(40)).
% 2.51/3.48 cnf('1.1.16.1.1.2',plain,[-(cC2(iV8476))],extension(42)).
% 2.51/3.48 cnf('1.1.16.2',plain,[-(cC2(20 ^ [iV8472])), cC32(iV8472)],extension(19,bind([[_31993], [iV8472]]))).
% 2.51/3.48 cnf('1.1.16.2.1',plain,[-(cC32(iV8472)), rR1(iV8472, iV8476), cC2(iV8476)],extension(20,bind([[_31993, _32081], [iV8472, iV8476]]))).
% 2.51/3.48 cnf('1.1.16.2.1.1',plain,[-(rR1(iV8472, iV8476))],extension(40)).
% 2.51/3.48 cnf('1.1.16.2.1.2',plain,[-(cC2(iV8476))],extension(42)).
% 2.51/3.48 cnf('1.1.17',plain,[-(cC60(iV8472)), cC2xcomp(iV8472), cC58(iV8472)],extension(25,bind([[_43057], [iV8472]]))).
% 2.51/3.48 cnf('1.1.17.1',plain,[-(cC2xcomp(iV8472))],extension(39)).
% 2.51/3.48 cnf('1.1.17.2',plain,[-(cC58(iV8472))],lemmata('1.1')).
% 2.51/3.48 cnf('1.1.18',plain,[-(cowlThing(iV8472))],extension(6,bind([[_24539], [iV8472]]))).
% 2.51/3.48 %-----------------------------------------------------
% 2.53/3.48
% 2.53/3.49 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------