%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KRS123+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n025.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:19 EDT 2023
% Result : Unsatisfiable 0.32s 1.39s
% Output : Proof 0.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : KRS123+1 : TPTP v8.1.2. Released v3.1.0.
% 0.04/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n025.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 18 23:08:18 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.32/1.39
% 0.32/1.39 /export/starexec/sandbox2/benchmark/theBenchmark.p is Unsatisfiable
% 0.32/1.39 Start of proof for negated /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.32/1.39 %-----------------------------------------------------
% 0.32/1.39 ncf(matrix, plain, [(2 ^ _13783) ^ [_13867] : [-(cowlThing(_13867))], (4 ^ _13783) ^ [_13909] : [cowlNothing(_13909)], (6 ^ _13783) ^ [_14032] : [xsd_string(_14032), xsd_integer(_14032)], (12 ^ _13783) ^ [_14185] : [-(xsd_integer(_14185)), -(xsd_string(_14185))], (18 ^ _13783) ^ [_14405] : [cUnsatisfiable(_14405), 21 ^ _13783 : [(22 ^ _13783) ^ [] : [-(cc(_14405))], (24 ^ _13783) ^ [] : [-(cd(_14405))]]], (26 ^ _13783) ^ [_14628] : [-(cUnsatisfiable(_14628)), cc(_14628), cd(_14628)], (36 ^ _13783) ^ [_14899] : [cc(_14899), -(cdxcomp(_14899))], (42 ^ _13783) ^ [_15085] : [cc1(_15085), -(cd1xcomp(_15085))], (48 ^ _13783) ^ [_15271] : [cc1(_15271), -(cd1(_15271))], (54 ^ _13783) ^ [_15486] : [cd(_15486), 57 ^ _13783 : [(58 ^ _13783) ^ [_15597] : [ra_Px1(_15486, _15597)]]], (60 ^ _13783) ^ [_15663] : [-(ra_Px1(_15663, 61 ^ [_15663])), -(cd(_15663))], (67 ^ _13783) ^ [_15936] : [cdxcomp(_15936), -(ra_Px1(_15936, 70 ^ [_15936]))], (74 ^ _13783) ^ [_16141] : [75 ^ _13783 : [(76 ^ _13783) ^ [_16208] : [ra_Px1(_16141, _16208)]], -(cdxcomp(_16141))], (80 ^ _13783) ^ [_16382] : [cd1(_16382), -(ra_Px2(_16382, 83 ^ [_16382]))], (87 ^ _13783) ^ [_16587] : [88 ^ _13783 : [(89 ^ _13783) ^ [_16654] : [ra_Px2(_16587, _16654)]], -(cd1(_16587))], (93 ^ _13783) ^ [_16828] : [cd1xcomp(_16828), 96 ^ _13783 : [(97 ^ _13783) ^ [_16939] : [ra_Px2(_16828, _16939)]]], (99 ^ _13783) ^ [_17005] : [-(ra_Px2(_17005, 100 ^ [_17005])), -(cd1xcomp(_17005))], (106 ^ _13783) ^ [_17249] : [ce3(_17249), -(cc(_17249))], (118 ^ _13783) ^ [] : [-(cUnsatisfiable(i2003_11_14_17_22_02803))], (112 ^ _13783) ^ [_17435] : [cf(_17435), -(cd(_17435))]], input).
% 0.32/1.39 ncf('1',plain,[cd(i2003_11_14_17_22_02803), 58 : ra_Px1(i2003_11_14_17_22_02803, 70 ^ [i2003_11_14_17_22_02803])],start(54 ^ 0,bind([[_15486, _15597], [i2003_11_14_17_22_02803, 70 ^ [i2003_11_14_17_22_02803]]]))).
% 0.32/1.39 ncf('1.1',plain,[-(cd(i2003_11_14_17_22_02803)), cUnsatisfiable(i2003_11_14_17_22_02803)],extension(18 ^ 1,bind([[_14405], [i2003_11_14_17_22_02803]]))).
% 0.32/1.39 ncf('1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_22_02803))],extension(118 ^ 2)).
% 0.32/1.39 ncf('1.2',plain,[-(ra_Px1(i2003_11_14_17_22_02803, 70 ^ [i2003_11_14_17_22_02803])), cdxcomp(i2003_11_14_17_22_02803)],extension(67 ^ 3,bind([[_15936], [i2003_11_14_17_22_02803]]))).
% 0.32/1.39 ncf('1.2.1',plain,[-(cdxcomp(i2003_11_14_17_22_02803)), cc(i2003_11_14_17_22_02803)],extension(36 ^ 4,bind([[_14899], [i2003_11_14_17_22_02803]]))).
% 0.32/1.39 ncf('1.2.1.1',plain,[-(cc(i2003_11_14_17_22_02803)), cUnsatisfiable(i2003_11_14_17_22_02803)],extension(18 ^ 5,bind([[_14405], [i2003_11_14_17_22_02803]]))).
% 0.32/1.39 ncf('1.2.1.1.1',plain,[-(cUnsatisfiable(i2003_11_14_17_22_02803))],extension(118 ^ 6)).
% 0.32/1.39 %-----------------------------------------------------
% 0.32/1.39 End of proof for negated /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------