%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : KRS160+1 : TPTP v8.1.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n032.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.22s 1.33s
% Output : Proof 0.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.08 % Problem : KRS160+1 : TPTP v8.1.0. Released v3.1.0.
% 0.04/0.08 % Command : leancop_casc.sh %s %d
% 0.07/0.27 % Computer : n032.cluster.edu
% 0.07/0.27 % Model : x86_64 x86_64
% 0.07/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.27 % Memory : 8042.1875MB
% 0.07/0.27 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.27 % CPULimit : 300
% 0.07/0.27 % WCLimit : 600
% 0.07/0.27 % DateTime : Tue Jun 7 08:29:20 EDT 2022
% 0.07/0.28 % CPUTime :
% 0.22/1.33 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.22/1.34 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.22/1.34
% 0.22/1.34 %-----------------------------------------------------
% 0.22/1.34 fof(the_axiom, conjecture, ! [_20195] : (cowlThing(_20195) & ~ cowlNothing(_20195)) & ! [_20195] : (xsd_string(_20195) <=> ~ xsd_integer(_20195)) & cowlThing(iV21080) & cC12(iV21080) & cC10(iV21081) & cowlThing(iV21081), file('/export/starexec/sandbox/benchmark/theBenchmark.p', the_axiom)).
% 0.22/1.34 fof(axiom_0, axiom, ! [_20529] : (cowlThing(_20529) & ~ cowlNothing(_20529)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_0)).
% 0.22/1.34 fof(axiom_1, axiom, ! [_20669] : (xsd_string(_20669) <=> ~ xsd_integer(_20669)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_1)).
% 0.22/1.34 fof(axiom_2, axiom, ! [_20811] : (cC10(_20811) <=> cC4(_20811) & cC2(_20811)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.22/1.34 fof(axiom_3, axiom, ! [_20955] : (cC12(_20955) <=> ? [_20970] : (rR1(_20955, _20970) & cC10(_20970))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.22/1.34 fof(axiom_17, axiom, rR1(iV21080, iV21081), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_17)).
% 0.22/1.34 fof(axiom_18, axiom, cC4(iV21081), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_18)).
% 0.22/1.34 fof(axiom_20, axiom, cC2(iV21081), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_20)).
% 0.22/1.34
% 0.22/1.34 cnf(1, plain, [-(12 ^ []), xsd_string(10 ^ [])], clausify(the_axiom)).
% 0.22/1.34 cnf(2, plain, [-(12 ^ []), xsd_integer(10 ^ [])], clausify(the_axiom)).
% 0.22/1.34 cnf(3, plain, [-(11 ^ []), -(xsd_integer(10 ^ []))], clausify(the_axiom)).
% 0.22/1.34 cnf(4, plain, [-(11 ^ []), -(xsd_string(10 ^ []))], clausify(the_axiom)).
% 0.22/1.34 cnf(5, plain, [-(cowlNothing(9 ^ [])), cowlThing(9 ^ []), 12 ^ [], 11 ^ [], cowlThing(iV21080), cC12(iV21080), cC10(iV21081), cowlThing(iV21081)], clausify(the_axiom)).
% 0.22/1.34 cnf(6, plain, [-(cowlThing(_5909))], clausify(axiom_0)).
% 0.22/1.34 cnf(7, plain, [cowlNothing(_5909)], clausify(axiom_0)).
% 0.22/1.34 cnf(8, plain, [xsd_string(_6137), xsd_integer(_6137)], clausify(axiom_1)).
% 0.22/1.34 cnf(9, plain, [-(xsd_string(_6137)), -(xsd_integer(_6137))], clausify(axiom_1)).
% 0.22/1.34 cnf(10, plain, [-(cC10(_6365)), cC4(_6365), cC2(_6365)], clausify(axiom_2)).
% 0.22/1.34 cnf(11, plain, [-(cC12(_6633)), rR1(_6633, _6721), cC10(_6721)], clausify(axiom_3)).
% 0.22/1.34 cnf(12, plain, [-(rR1(iV21080, iV21081))], clausify(axiom_17)).
% 0.22/1.34 cnf(13, plain, [-(cC4(iV21081))], clausify(axiom_18)).
% 0.22/1.34 cnf(14, plain, [-(cC2(iV21081))], clausify(axiom_20)).
% 0.22/1.34
% 0.22/1.34 cnf('1',plain,[cowlNothing(9 ^ [])],start(7,bind([[_5909], [9 ^ []]]))).
% 0.22/1.34 cnf('1.1',plain,[-(cowlNothing(9 ^ [])), cowlThing(9 ^ []), 12 ^ [], 11 ^ [], cowlThing(iV21080), cC12(iV21080), cC10(iV21081), cowlThing(iV21081)],extension(5)).
% 0.22/1.34 cnf('1.1.1',plain,[-(cowlThing(9 ^ []))],extension(6,bind([[_5909], [9 ^ []]]))).
% 0.22/1.34 cnf('1.1.2',plain,[-(12 ^ []), xsd_string(10 ^ [])],extension(1)).
% 0.22/1.34 cnf('1.1.2.1',plain,[-(xsd_string(10 ^ [])), -(xsd_integer(10 ^ []))],extension(9,bind([[_6137], [10 ^ []]]))).
% 0.22/1.34 cnf('1.1.2.1.1',plain,[xsd_integer(10 ^ []), -(12 ^ [])],extension(2)).
% 0.22/1.34 cnf('1.1.2.1.1.1',plain,[12 ^ []],reduction('1.1')).
% 0.22/1.34 cnf('1.1.3',plain,[-(11 ^ []), -(xsd_integer(10 ^ []))],extension(3)).
% 0.22/1.34 cnf('1.1.3.1',plain,[xsd_integer(10 ^ []), xsd_string(10 ^ [])],extension(8,bind([[_6137], [10 ^ []]]))).
% 0.22/1.34 cnf('1.1.3.1.1',plain,[-(xsd_string(10 ^ [])), -(11 ^ [])],extension(4)).
% 0.22/1.34 cnf('1.1.3.1.1.1',plain,[11 ^ []],reduction('1.1')).
% 0.22/1.34 cnf('1.1.4',plain,[-(cowlThing(iV21080))],extension(6,bind([[_5909], [iV21080]]))).
% 0.22/1.34 cnf('1.1.5',plain,[-(cC12(iV21080)), rR1(iV21080, iV21081), cC10(iV21081)],extension(11,bind([[_6633, _6721], [iV21080, iV21081]]))).
% 0.22/1.34 cnf('1.1.5.1',plain,[-(rR1(iV21080, iV21081))],extension(12)).
% 0.22/1.34 cnf('1.1.5.2',plain,[-(cC10(iV21081)), cC4(iV21081), cC2(iV21081)],extension(10,bind([[_6365], [iV21081]]))).
% 0.22/1.34 cnf('1.1.5.2.1',plain,[-(cC4(iV21081))],extension(13)).
% 0.22/1.34 cnf('1.1.5.2.2',plain,[-(cC2(iV21081))],extension(14)).
% 0.22/1.34 cnf('1.1.6',plain,[-(cC10(iV21081)), cC4(iV21081), cC2(iV21081)],extension(10,bind([[_6365], [iV21081]]))).
% 0.22/1.34 cnf('1.1.6.1',plain,[-(cC4(iV21081))],extension(13)).
% 0.22/1.34 cnf('1.1.6.2',plain,[-(cC2(iV21081))],extension(14)).
% 0.22/1.34 cnf('1.1.7',plain,[-(cowlThing(iV21081))],extension(6,bind([[_5909], [iV21081]]))).
% 0.22/1.34 %-----------------------------------------------------
% 0.22/1.35
% 0.22/1.35 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------