%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS100+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n013.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 : 300s
% DateTime : Fri May 19 11:26:16 EDT 2023
% Result : Unsatisfiable 0.21s 1.33s
% Output : Proof 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.10 % Problem : KRS100+1 : TPTP v8.1.2. Released v3.1.0.
% 0.02/0.11 % Command : nanocop.sh %s %d
% 0.11/0.30 % Computer : n013.cluster.edu
% 0.11/0.30 % Model : x86_64 x86_64
% 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.30 % Memory : 8042.1875MB
% 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.30 % CPULimit : 300
% 0.11/0.30 % WCLimit : 300
% 0.11/0.30 % DateTime : Thu May 18 23:00:20 EDT 2023
% 0.11/0.30 % CPUTime :
% 0.21/1.33
% 0.21/1.33 /export/starexec/sandbox2/benchmark/theBenchmark.p is Unsatisfiable
% 0.21/1.33 Start of proof for negated /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/1.33 %-----------------------------------------------------
% 0.21/1.33 ncf(matrix, plain, [(2 ^ _9642) ^ [_9726] : [-(cowlThing(_9726))], (4 ^ _9642) ^ [_9768] : [cowlNothing(_9768)], (6 ^ _9642) ^ [_9891] : [xsd_string(_9891), xsd_integer(_9891)], (12 ^ _9642) ^ [_10044] : [-(xsd_integer(_10044)), -(xsd_string(_10044))], (75 ^ _9642) ^ [] : [-(cUnsatisfiable(i2003_11_14_17_20_32704))], (69 ^ _9642) ^ [_11939] : [cc(_11939), cd(_11939)], (43 ^ _9642) ^ [_11083] : [-(cUnsatisfiable(_11083)), 47 ^ _9642 : [(48 ^ _9642) ^ [] : [-(rr(_11083, 46 ^ [_11083]))], (50 ^ _9642) ^ [] : [ce(46 ^ [_11083])], (52 ^ _9642) ^ [] : [-(cd(46 ^ [_11083]))]], 56 ^ _9642 : [(57 ^ _9642) ^ [] : [-(rr(_11083, 55 ^ [_11083]))], (59 ^ _9642) ^ [] : [cd(55 ^ [_11083])]], 60 ^ _9642 : [(61 ^ _9642) ^ [_11681] : [rr(_11083, _11681), -(ce(_11681))]]], (18 ^ _9642) ^ [_10264] : [cUnsatisfiable(_10264), 21 ^ _9642 : [(39 ^ _9642) ^ [] : [-(rr(_10264, 37 ^ [_10264]))], (41 ^ _9642) ^ [] : [ce(37 ^ [_10264])], (32 ^ _9642) ^ [_10740] : [rr(_10264, _10740), -(cd(_10740))], (22 ^ _9642) ^ [_10455] : [rr(_10264, _10455), -(ce(_10455)), cd(_10455)]]]], input).
% 0.21/1.33 ncf('1',plain,[cUnsatisfiable(i2003_11_14_17_20_32704), 41 : ce(37 ^ [i2003_11_14_17_20_32704])],start(18 ^ 0,bind([[_10264], [i2003_11_14_17_20_32704]]))).
% 0.21/1.33 ncf('1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_20_32704))],extension(75 ^ 1)).
% 0.21/1.33 ncf('1.2',plain,[-(ce(37 ^ [i2003_11_14_17_20_32704])), rr(i2003_11_14_17_20_32704, 37 ^ [i2003_11_14_17_20_32704]), cd(37 ^ [i2003_11_14_17_20_32704])],extension(22 ^ 3,bind([[_10455], [37 ^ [i2003_11_14_17_20_32704]]]))).
% 0.21/1.33 ncf('1.2.1',plain,[-(rr(i2003_11_14_17_20_32704, 37 ^ [i2003_11_14_17_20_32704]))],extension(39 ^ 4)).
% 0.21/1.33 ncf('1.2.2',plain,[-(cd(37 ^ [i2003_11_14_17_20_32704])), rr(i2003_11_14_17_20_32704, 37 ^ [i2003_11_14_17_20_32704])],extension(32 ^ 4,bind([[_10740], [37 ^ [i2003_11_14_17_20_32704]]]))).
% 0.21/1.33 ncf('1.2.2.1',plain,[-(rr(i2003_11_14_17_20_32704, 37 ^ [i2003_11_14_17_20_32704]))],lemmata('[1].x')).
% 0.21/1.33 %-----------------------------------------------------
% 0.21/1.33 End of proof for negated /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------