%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : PUZ132+1 : TPTP v8.1.2. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n008.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:48:03 EDT 2023
% Result : Theorem 0.34s 1.37s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : PUZ132+1 : TPTP v8.1.2. Released v4.1.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.13/0.32 % Computer : n008.cluster.edu
% 0.13/0.32 % Model : x86_64 x86_64
% 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.32 % Memory : 8042.1875MB
% 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.32 % CPULimit : 300
% 0.13/0.32 % WCLimit : 300
% 0.13/0.32 % DateTime : Thu May 18 20:03:09 EDT 2023
% 0.13/0.33 % CPUTime :
% 0.34/1.37
% 0.34/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.34/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.34/1.37 %-----------------------------------------------------
% 0.34/1.37 ncf(matrix, plain, [(115 ^ _16389) ^ [] : [beautiful(washington), has_crime(washington)], (77 ^ _16389) ^ [] : [-(capital(75 ^ []))], (80 ^ _16389) ^ [] : [-(city(78 ^ []))], (82 ^ _16389) ^ [_18990] : [capital(_18990), -(city(_18990))], (89 ^ _16389) ^ [] : [-(country(87 ^ []))], (91 ^ _16389) ^ [] : [-(capital(washington))], (93 ^ _16389) ^ [] : [-(country(usa))], (95 ^ _16389) ^ [_19371] : [country(_19371), -(capital(capital_city(_19371)))], (101 ^ _16389) ^ [_19561] : [city(_19561), -(has_crime(_19561))], (107 ^ _16389) ^ [] : [-(capital_city(usa) = washington)], (109 ^ _16389) ^ [_19780] : [country(_19780), -(beautiful(capital_city(_19780)))], (70 ^ _16389) ^ [_18606, _18608] : [_18608 = _18606, -(capital_city(_18608) = capital_city(_18606))], (2 ^ _16389) ^ [_16533] : [-(_16533 = _16533)], (4 ^ _16389) ^ [_16640, _16642] : [_16642 = _16640, -(_16640 = _16642)], (10 ^ _16389) ^ [_16844, _16846, _16848] : [-(_16848 = _16844), _16848 = _16846, _16846 = _16844], (20 ^ _16389) ^ [_17157, _17159] : [-(capital(_17157)), _17159 = _17157, capital(_17159)], (30 ^ _16389) ^ [_17452, _17454] : [-(city(_17452)), _17454 = _17452, city(_17454)], (40 ^ _16389) ^ [_17747, _17749] : [-(country(_17747)), _17749 = _17747, country(_17749)], (50 ^ _16389) ^ [_18042, _18044] : [-(beautiful(_18042)), _18044 = _18042, beautiful(_18044)], (60 ^ _16389) ^ [_18317, _18319] : [-(has_crime(_18317)), _18319 = _18317, has_crime(_18319)]], input).
% 0.34/1.37 ncf('1',plain,[beautiful(washington), has_crime(washington)],start(115 ^ 0)).
% 0.34/1.37 ncf('1.1',plain,[-(beautiful(washington)), capital_city(usa) = washington, beautiful(capital_city(usa))],extension(50 ^ 1,bind([[_18042, _18044], [washington, capital_city(usa)]]))).
% 0.34/1.37 ncf('1.1.1',plain,[-(capital_city(usa) = washington)],extension(107 ^ 2)).
% 0.34/1.37 ncf('1.1.2',plain,[-(beautiful(capital_city(usa))), country(usa)],extension(109 ^ 2,bind([[_19780], [usa]]))).
% 0.34/1.37 ncf('1.1.2.1',plain,[-(country(usa))],extension(93 ^ 3)).
% 0.34/1.37 ncf('1.2',plain,[-(has_crime(washington)), city(washington)],extension(101 ^ 1,bind([[_19561], [washington]]))).
% 0.34/1.37 ncf('1.2.1',plain,[-(city(washington)), capital(washington)],extension(82 ^ 2,bind([[_18990], [washington]]))).
% 0.34/1.37 ncf('1.2.1.1',plain,[-(capital(washington))],extension(91 ^ 3)).
% 0.34/1.37 %-----------------------------------------------------
% 0.34/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------