%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS169+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n007.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:25 EDT 2023
% Result : Theorem 0.33s 1.40s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : KRS169+1 : TPTP v8.1.2. Released v3.1.0.
% 0.12/0.13 % Command : nanocop.sh %s %d
% 0.13/0.35 % Computer : n007.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 18 22:51:08 EDT 2023
% 0.13/0.35 % CPUTime :
% 0.33/1.40
% 0.33/1.40 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.33/1.40 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.33/1.40 %-----------------------------------------------------
% 0.33/1.40 ncf(matrix, plain, [(36 ^ _9473) ^ [] : [cowlThing(37 ^ []), -(cowlNothing(37 ^ [])), 49 ^ _9473 : [(50 ^ _9473) ^ [] : [-(xsd_string(46 ^ []))], (52 ^ _9473) ^ [] : [-(xsd_integer(46 ^ []))]], 53 ^ _9473 : [(54 ^ _9473) ^ [] : [xsd_integer(46 ^ [])], (56 ^ _9473) ^ [] : [xsd_string(46 ^ [])]], cowlThing(iX), rhasHead(iX, iY), cowlThing(iY)], (2 ^ _9473) ^ [_9577] : [-(cowlThing(_9577))], (4 ^ _9473) ^ [_9619] : [cowlNothing(_9619)], (6 ^ _9473) ^ [_9742] : [xsd_string(_9742), xsd_integer(_9742)], (12 ^ _9473) ^ [_9895] : [-(xsd_integer(_9895)), -(xsd_string(_9895))], (18 ^ _9473) ^ [] : [-(cowlThing(iX))], (20 ^ _9473) ^ [] : [-(rhasLeader(iX, iY))], (22 ^ _9473) ^ [] : [-(cowlThing(iY))], (24 ^ _9473) ^ [_10268, _10270] : [rhasLeader(_10270, _10268), -(rhasHead(_10270, _10268))], (30 ^ _9473) ^ [_10430, _10432] : [rhasHead(_10432, _10430), -(rhasLeader(_10432, _10430))]], input).
% 0.33/1.40 ncf('1',plain,[cowlNothing(37 ^ [])],start(4 ^ 0,bind([[_9619], [37 ^ []]]))).
% 0.33/1.40 ncf('1.1',plain,[-(cowlNothing(37 ^ [])), cowlThing(37 ^ []), 50 : -(xsd_string(46 ^ [])), 54 : xsd_integer(46 ^ []), 54 : cowlThing(iX), 54 : rhasHead(iX, iY), 54 : cowlThing(iY)],extension(36 ^ 1)).
% 0.33/1.40 ncf('1.1.1',plain,[-(cowlThing(37 ^ []))],extension(2 ^ 2,bind([[_9577], [37 ^ []]]))).
% 0.33/1.40 ncf('1.1.2',plain,[xsd_string(46 ^ []), xsd_integer(46 ^ [])],extension(6 ^ 4,bind([[_9742], [46 ^ []]]))).
% 0.33/1.40 ncf('1.1.2.1',plain,[-(xsd_integer(46 ^ []))],extension(52 ^ 5)).
% 0.33/1.40 ncf('1.1.3',plain,[-(xsd_integer(46 ^ [])), -(xsd_string(46 ^ []))],extension(12 ^ 4,bind([[_9895], [46 ^ []]]))).
% 0.33/1.40 ncf('1.1.3.1',plain,[xsd_string(46 ^ [])],extension(56 ^ 5)).
% 0.33/1.40 ncf('1.1.4',plain,[-(cowlThing(iX))],extension(2 ^ 2,bind([[_9577], [iX]]))).
% 0.33/1.40 ncf('1.1.5',plain,[-(rhasHead(iX, iY)), rhasLeader(iX, iY)],extension(24 ^ 2,bind([[_10268, _10270], [iY, iX]]))).
% 0.33/1.40 ncf('1.1.5.1',plain,[-(rhasLeader(iX, iY))],extension(20 ^ 3)).
% 0.33/1.40 ncf('1.1.6',plain,[-(cowlThing(iY))],extension(2 ^ 2,bind([[_9577], [iY]]))).
% 0.33/1.40 %-----------------------------------------------------
% 0.33/1.40 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------