%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : KRS158+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n028.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 0.32s 1.40s
% Output : Proof 0.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : KRS158+1 : TPTP v8.1.0. Released v3.1.0.
% 0.06/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n028.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 : Tue Jun 7 14:18:30 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.32/1.40 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.32/1.41 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.32/1.41
% 0.32/1.41 %-----------------------------------------------------
% 0.32/1.41 fof(the_axiom, conjecture, ! [_27948] : (cowlThing(_27948) & ~ cowlNothing(_27948)) & ! [_27948] : (xsd_string(_27948) <=> ~ xsd_integer(_27948)) & cC18(iV16560) & cC14(iV16560) & cC8(iV16560) & cC16(iV16560) & cowlThing(iV16560) & cC6(iV16561) & cowlThing(iV16561) & cC12(iV16562) & cowlThing(iV16562), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', the_axiom)).
% 0.32/1.41 fof(axiom_0, axiom, ! [_28387] : (cowlThing(_28387) & ~ cowlNothing(_28387)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_0)).
% 0.32/1.41 fof(axiom_1, axiom, ! [_28527] : (xsd_string(_28527) <=> ~ xsd_integer(_28527)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_1)).
% 0.32/1.41 fof(axiom_5, axiom, ! [_28676] : (cC12(_28676) <=> cC10xcomp(_28676) & cC2xcomp(_28676)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_5)).
% 0.32/1.41 fof(axiom_6, axiom, ! [_28820] : (cC14(_28820) <=> ? [_28835] : (rR1(_28820, _28835) & cC12(_28835))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_6)).
% 0.32/1.41 fof(axiom_7, axiom, ! [_29000] : (cC16(_29000) <=> cC14(_29000) & cC8(_29000)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_7)).
% 0.32/1.41 fof(axiom_8, axiom, ! [_29155] : (cC18(_29155) <=> cTOP(_29155) & cC16(_29155)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_8)).
% 0.32/1.41 fof(axiom_14, axiom, ! [_29311] : (cC6(_29311) <=> cC4xcomp(_29311) & cC2xcomp(_29311)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_14)).
% 0.32/1.41 fof(axiom_18, axiom, cTEST(iV16560), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_18)).
% 0.32/1.41 fof(axiom_20, axiom, rR1(iV16560, iV16562), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_20)).
% 0.32/1.41 fof(axiom_24, axiom, cC4xcomp(iV16561), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_24)).
% 0.32/1.41 fof(axiom_25, axiom, cC2xcomp(iV16561), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_25)).
% 0.32/1.41 fof(axiom_28, axiom, cC10xcomp(iV16562), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_28)).
% 0.32/1.41 fof(axiom_29, axiom, cC2xcomp(iV16562), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_29)).
% 0.32/1.41 fof(axiom_16, axiom, ! [_29749] : (cTEST(_29749) <=> cTOP(_29749) & cC18(_29749)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_16)).
% 0.32/1.41
% 0.32/1.41 cnf(1, plain, [-(14 ^ []), xsd_string(12 ^ [])], clausify(the_axiom)).
% 0.32/1.41 cnf(2, plain, [-(14 ^ []), xsd_integer(12 ^ [])], clausify(the_axiom)).
% 0.32/1.41 cnf(3, plain, [-(13 ^ []), -(xsd_integer(12 ^ []))], clausify(the_axiom)).
% 0.32/1.41 cnf(4, plain, [-(13 ^ []), -(xsd_string(12 ^ []))], clausify(the_axiom)).
% 0.32/1.41 cnf(5, plain, [-(cowlNothing(11 ^ [])), cowlThing(11 ^ []), 14 ^ [], 13 ^ [], cC18(iV16560), cC14(iV16560), cC8(iV16560), cC16(iV16560), cowlThing(iV16560), cC6(iV16561), cowlThing(iV16561), cC12(iV16562), cowlThing(iV16562)], clausify(the_axiom)).
% 0.32/1.41 cnf(6, plain, [-(cowlThing(_7170))], clausify(axiom_0)).
% 0.32/1.41 cnf(7, plain, [cowlNothing(_7170)], clausify(axiom_0)).
% 0.32/1.41 cnf(8, plain, [xsd_string(_7398), xsd_integer(_7398)], clausify(axiom_1)).
% 0.32/1.41 cnf(9, plain, [-(xsd_string(_7398)), -(xsd_integer(_7398))], clausify(axiom_1)).
% 0.32/1.41 cnf(10, plain, [-(cC12(_8556)), cC10xcomp(_8556), cC2xcomp(_8556)], clausify(axiom_5)).
% 0.32/1.41 cnf(11, plain, [-(cC14(_8824)), rR1(_8824, _8912), cC12(_8912)], clausify(axiom_6)).
% 0.32/1.41 cnf(12, plain, [cC16(_9170), -(cC8(_9170))], clausify(axiom_7)).
% 0.32/1.41 cnf(13, plain, [-(cC16(_9170)), cC14(_9170), cC8(_9170)], clausify(axiom_7)).
% 0.32/1.41 cnf(14, plain, [cC18(_9438), -(cC16(_9438))], clausify(axiom_8)).
% 0.32/1.41 cnf(15, plain, [-(cC6(_11220)), cC4xcomp(_11220), cC2xcomp(_11220)], clausify(axiom_14)).
% 0.32/1.41 cnf(16, plain, [-(cTEST(iV16560))], clausify(axiom_18)).
% 0.32/1.41 cnf(17, plain, [-(rR1(iV16560, iV16562))], clausify(axiom_20)).
% 0.32/1.41 cnf(18, plain, [-(cC4xcomp(iV16561))], clausify(axiom_24)).
% 0.32/1.41 cnf(19, plain, [-(cC2xcomp(iV16561))], clausify(axiom_25)).
% 0.32/1.41 cnf(20, plain, [-(cC10xcomp(iV16562))], clausify(axiom_28)).
% 0.32/1.41 cnf(21, plain, [-(cC2xcomp(iV16562))], clausify(axiom_29)).
% 0.32/1.41 cnf(22, plain, [cTEST(_11834), -(cC18(_11834))], clausify(axiom_16)).
% 0.32/1.41
% 0.32/1.41 cnf('1',plain,[cowlNothing(11 ^ [])],start(7,bind([[_7170], [11 ^ []]]))).
% 0.32/1.41 cnf('1.1',plain,[-(cowlNothing(11 ^ [])), cowlThing(11 ^ []), 14 ^ [], 13 ^ [], cC18(iV16560), cC14(iV16560), cC8(iV16560), cC16(iV16560), cowlThing(iV16560), cC6(iV16561), cowlThing(iV16561), cC12(iV16562), cowlThing(iV16562)],extension(5)).
% 0.32/1.41 cnf('1.1.1',plain,[-(cowlThing(11 ^ []))],extension(6,bind([[_7170], [11 ^ []]]))).
% 0.32/1.41 cnf('1.1.2',plain,[-(14 ^ []), xsd_string(12 ^ [])],extension(1)).
% 0.32/1.41 cnf('1.1.2.1',plain,[-(xsd_string(12 ^ [])), -(xsd_integer(12 ^ []))],extension(9,bind([[_7398], [12 ^ []]]))).
% 0.32/1.41 cnf('1.1.2.1.1',plain,[xsd_integer(12 ^ []), -(14 ^ [])],extension(2)).
% 0.32/1.41 cnf('1.1.2.1.1.1',plain,[14 ^ []],reduction('1.1')).
% 0.32/1.41 cnf('1.1.3',plain,[-(13 ^ []), -(xsd_integer(12 ^ []))],extension(3)).
% 0.32/1.41 cnf('1.1.3.1',plain,[xsd_integer(12 ^ []), xsd_string(12 ^ [])],extension(8,bind([[_7398], [12 ^ []]]))).
% 0.32/1.41 cnf('1.1.3.1.1',plain,[-(xsd_string(12 ^ [])), -(13 ^ [])],extension(4)).
% 0.32/1.41 cnf('1.1.3.1.1.1',plain,[13 ^ []],reduction('1.1')).
% 0.32/1.41 cnf('1.1.4',plain,[-(cC18(iV16560)), cTEST(iV16560)],extension(22,bind([[_11834], [iV16560]]))).
% 0.32/1.41 cnf('1.1.4.1',plain,[-(cTEST(iV16560))],extension(16)).
% 0.32/1.41 cnf('1.1.5',plain,[-(cC14(iV16560)), rR1(iV16560, iV16562), cC12(iV16562)],extension(11,bind([[_8824, _8912], [iV16560, iV16562]]))).
% 0.32/1.41 cnf('1.1.5.1',plain,[-(rR1(iV16560, iV16562))],extension(17)).
% 0.32/1.41 cnf('1.1.5.2',plain,[-(cC12(iV16562)), cC10xcomp(iV16562), cC2xcomp(iV16562)],extension(10,bind([[_8556], [iV16562]]))).
% 0.32/1.41 cnf('1.1.5.2.1',plain,[-(cC10xcomp(iV16562))],extension(20)).
% 0.32/1.41 cnf('1.1.5.2.2',plain,[-(cC2xcomp(iV16562))],extension(21)).
% 0.32/1.41 cnf('1.1.6',plain,[-(cC8(iV16560)), cC16(iV16560)],extension(12,bind([[_9170], [iV16560]]))).
% 0.32/1.41 cnf('1.1.6.1',plain,[-(cC16(iV16560)), cC18(iV16560)],extension(14,bind([[_9438], [iV16560]]))).
% 0.32/1.41 cnf('1.1.6.1.1',plain,[-(cC18(iV16560))],lemmata('1.1')).
% 0.32/1.41 cnf('1.1.7',plain,[-(cC16(iV16560)), cC14(iV16560), cC8(iV16560)],extension(13,bind([[_9170], [iV16560]]))).
% 0.32/1.41 cnf('1.1.7.1',plain,[-(cC14(iV16560))],lemmata('1.1')).
% 0.32/1.41 cnf('1.1.7.2',plain,[-(cC8(iV16560))],lemmata('1.1')).
% 0.32/1.41 cnf('1.1.8',plain,[-(cowlThing(iV16560))],extension(6,bind([[_7170], [iV16560]]))).
% 0.32/1.41 cnf('1.1.9',plain,[-(cC6(iV16561)), cC4xcomp(iV16561), cC2xcomp(iV16561)],extension(15,bind([[_11220], [iV16561]]))).
% 0.32/1.41 cnf('1.1.9.1',plain,[-(cC4xcomp(iV16561))],extension(18)).
% 0.32/1.41 cnf('1.1.9.2',plain,[-(cC2xcomp(iV16561))],extension(19)).
% 0.32/1.41 cnf('1.1.10',plain,[-(cowlThing(iV16561))],extension(6,bind([[_7170], [iV16561]]))).
% 0.32/1.41 cnf('1.1.11',plain,[-(cC12(iV16562)), cC10xcomp(iV16562), cC2xcomp(iV16562)],extension(10,bind([[_8556], [iV16562]]))).
% 0.32/1.41 cnf('1.1.11.1',plain,[-(cC10xcomp(iV16562))],extension(20)).
% 0.32/1.41 cnf('1.1.11.2',plain,[-(cC2xcomp(iV16562))],extension(21)).
% 0.32/1.41 cnf('1.1.12',plain,[-(cowlThing(iV16562))],extension(6,bind([[_7170], [iV16562]]))).
% 0.32/1.41 %-----------------------------------------------------
% 0.39/1.42
% 0.39/1.42 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------