%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : ALG030+1 : TPTP v8.1.2. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n024.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 10:07:55 EDT 2023
% Result : Theorem 0.88s 1.40s
% Output : Proof 0.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : ALG030+1 : TPTP v8.1.2. Released v2.7.0.
% 0.12/0.13 % Command : nanocop.sh %s %d
% 0.14/0.35 % Computer : n024.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 18 23:33:21 EDT 2023
% 0.14/0.35 % CPUTime :
% 0.88/1.40
% 0.88/1.40 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.88/1.40 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.88/1.40 %-----------------------------------------------------
% 0.88/1.40 ncf(matrix, plain, [(110 ^ _27787) ^ [_31580] : [sorti1(_31580), -(sorti2(h(_31580)))], (116 ^ _27787) ^ [_31750] : [sorti2(_31750), -(sorti1(j(_31750)))], (122 ^ _27787) ^ [_31942] : [sorti1(_31942), 125 ^ _27787 : [(126 ^ _27787) ^ [_32084] : [sorti1(_32084), -(h(op1(_31942, _32084)) = op2(h(_31942), h(_32084)))]]], (132 ^ _27787) ^ [_32309] : [sorti2(_32309), 135 ^ _27787 : [(136 ^ _27787) ^ [_32451] : [sorti2(_32451), -(j(op2(_32309, _32451)) = op1(j(_32309), j(_32451)))]]], (142 ^ _27787) ^ [_32676] : [sorti2(_32676), -(h(j(_32676)) = _32676)], (148 ^ _27787) ^ [_32852] : [sorti1(_32852), -(j(h(_32852)) = _32852)], (72 ^ _27787) ^ [_30267] : [sorti1(_30267), 75 ^ _27787 : [(76 ^ _27787) ^ [_30399] : [sorti1(_30399), -(sorti1(op1(_30267, _30399)))]]], (82 ^ _27787) ^ [_30604] : [sorti2(_30604), 85 ^ _27787 : [(86 ^ _27787) ^ [_30736] : [sorti2(_30736), -(sorti2(op2(_30604, _30736)))]]], (93 ^ _27787) ^ [] : [-(sorti1(91 ^ []))], (96 ^ _27787) ^ [] : [-(sorti1(94 ^ []))], (98 ^ _27787) ^ [] : [op1(91 ^ [], 94 ^ []) = op1(94 ^ [], 91 ^ [])], (100 ^ _27787) ^ [_31189] : [sorti2(_31189), 103 ^ _27787 : [(104 ^ _27787) ^ [_31325] : [sorti2(_31325), -(op2(_31189, _31325) = op2(_31325, _31189))]]], (40 ^ _27787) ^ [_29161, _29163, _29165, _29167] : [-(op2(_29167, _29163) = op2(_29165, _29161)), _29167 = _29165, _29163 = _29161], (50 ^ _27787) ^ [_29520, _29522, _29524, _29526] : [-(op1(_29526, _29522) = op1(_29524, _29520)), _29526 = _29524, _29522 = _29520], (60 ^ _27787) ^ [_29851, _29853] : [_29853 = _29851, -(j(_29853) = j(_29851))], (66 ^ _27787) ^ [_30049, _30051] : [_30051 = _30049, -(h(_30051) = h(_30049))], (2 ^ _27787) ^ [_27931] : [-(_27931 = _27931)], (4 ^ _27787) ^ [_28038, _28040] : [_28040 = _28038, -(_28038 = _28040)], (10 ^ _27787) ^ [_28242, _28244, _28246] : [-(_28246 = _28242), _28246 = _28244, _28244 = _28242], (20 ^ _27787) ^ [_28555, _28557] : [-(sorti2(_28555)), _28557 = _28555, sorti2(_28557)], (30 ^ _27787) ^ [_28830, _28832] : [-(sorti1(_28830)), _28832 = _28830, sorti1(_28832)]], input).
% 0.88/1.40 ncf('1',plain,[op1(91 ^ [], 94 ^ []) = op1(94 ^ [], 91 ^ [])],start(98 ^ 0)).
% 0.88/1.40 ncf('1.1',plain,[-(op1(91 ^ [], 94 ^ []) = op1(94 ^ [], 91 ^ [])), op1(91 ^ [], 94 ^ []) = j(op2(h(91 ^ []), h(94 ^ []))), j(op2(h(91 ^ []), h(94 ^ []))) = op1(94 ^ [], 91 ^ [])],extension(10 ^ 1,bind([[_28242, _28244, _28246], [op1(94 ^ [], 91 ^ []), j(op2(h(91 ^ []), h(94 ^ []))), op1(91 ^ [], 94 ^ [])]]))).
% 0.88/1.40 ncf('1.1.1',plain,[-(op1(91 ^ [], 94 ^ []) = j(op2(h(91 ^ []), h(94 ^ [])))), j(op2(h(91 ^ []), h(94 ^ []))) = op1(91 ^ [], 94 ^ [])],extension(4 ^ 2,bind([[_28038, _28040], [op1(91 ^ [], 94 ^ []), j(op2(h(91 ^ []), h(94 ^ [])))]]))).
% 0.88/1.40 ncf('1.1.1.1',plain,[-(j(op2(h(91 ^ []), h(94 ^ []))) = op1(91 ^ [], 94 ^ [])), j(op2(h(91 ^ []), h(94 ^ []))) = op1(j(h(91 ^ [])), j(h(94 ^ []))), op1(j(h(91 ^ [])), j(h(94 ^ []))) = op1(91 ^ [], 94 ^ [])],extension(10 ^ 3,bind([[_28242, _28244, _28246], [op1(91 ^ [], 94 ^ []), op1(j(h(91 ^ [])), j(h(94 ^ []))), j(op2(h(91 ^ []), h(94 ^ [])))]]))).
% 0.88/1.40 ncf('1.1.1.1.1',plain,[-(j(op2(h(91 ^ []), h(94 ^ []))) = op1(j(h(91 ^ [])), j(h(94 ^ [])))), 136 : sorti2(h(94 ^ [])), 136 : sorti2(h(91 ^ []))],extension(132 ^ 4,bind([[_32309, _32451], [h(91 ^ []), h(94 ^ [])]]))).
% 0.88/1.40 ncf('1.1.1.1.1.1',plain,[-(sorti2(h(94 ^ []))), sorti1(94 ^ [])],extension(110 ^ 7,bind([[_31580], [94 ^ []]]))).
% 0.88/1.40 ncf('1.1.1.1.1.1.1',plain,[-(sorti1(94 ^ []))],extension(96 ^ 8)).
% 0.88/1.40 ncf('1.1.1.1.1.2',plain,[-(sorti2(h(91 ^ []))), sorti1(91 ^ [])],extension(110 ^ 5,bind([[_31580], [91 ^ []]]))).
% 0.88/1.40 ncf('1.1.1.1.1.2.1',plain,[-(sorti1(91 ^ []))],extension(93 ^ 6)).
% 0.88/1.40 ncf('1.1.1.1.2',plain,[-(op1(j(h(91 ^ [])), j(h(94 ^ []))) = op1(91 ^ [], 94 ^ [])), j(h(91 ^ [])) = 91 ^ [], j(h(94 ^ [])) = 94 ^ []],extension(50 ^ 4,bind([[_29520, _29522, _29524, _29526], [94 ^ [], j(h(94 ^ [])), 91 ^ [], j(h(91 ^ []))]]))).
% 0.88/1.40 ncf('1.1.1.1.2.1',plain,[-(j(h(91 ^ [])) = 91 ^ []), sorti1(91 ^ [])],extension(148 ^ 5,bind([[_32852], [91 ^ []]]))).
% 0.88/1.40 ncf('1.1.1.1.2.1.1',plain,[-(sorti1(91 ^ []))],extension(93 ^ 6)).
% 0.88/1.40 ncf('1.1.1.1.2.2',plain,[-(j(h(94 ^ [])) = 94 ^ []), sorti1(94 ^ [])],extension(148 ^ 5,bind([[_32852], [94 ^ []]]))).
% 0.88/1.40 ncf('1.1.1.1.2.2.1',plain,[-(sorti1(94 ^ []))],extension(96 ^ 6)).
% 0.88/1.40 ncf('1.1.2',plain,[-(j(op2(h(91 ^ []), h(94 ^ []))) = op1(94 ^ [], 91 ^ [])), j(op2(h(91 ^ []), h(94 ^ []))) = j(op2(h(94 ^ []), h(91 ^ []))), j(op2(h(94 ^ []), h(91 ^ []))) = op1(94 ^ [], 91 ^ [])],extension(10 ^ 2,bind([[_28242, _28244, _28246], [op1(94 ^ [], 91 ^ []), j(op2(h(94 ^ []), h(91 ^ []))), j(op2(h(91 ^ []), h(94 ^ [])))]]))).
% 0.88/1.40 ncf('1.1.2.1',plain,[-(j(op2(h(91 ^ []), h(94 ^ []))) = j(op2(h(94 ^ []), h(91 ^ [])))), op2(h(91 ^ []), h(94 ^ [])) = op2(h(94 ^ []), h(91 ^ []))],extension(60 ^ 3,bind([[_29851, _29853], [op2(h(94 ^ []), h(91 ^ [])), op2(h(91 ^ []), h(94 ^ []))]]))).
% 0.88/1.40 ncf('1.1.2.1.1',plain,[-(op2(h(91 ^ []), h(94 ^ [])) = op2(h(94 ^ []), h(91 ^ []))), 104 : sorti2(h(94 ^ [])), 104 : sorti2(h(91 ^ []))],extension(100 ^ 4,bind([[_31189, _31325], [h(91 ^ []), h(94 ^ [])]]))).
% 0.88/1.40 ncf('1.1.2.1.1.1',plain,[-(sorti2(h(94 ^ []))), sorti1(94 ^ [])],extension(110 ^ 7,bind([[_31580], [94 ^ []]]))).
% 0.88/1.40 ncf('1.1.2.1.1.1.1',plain,[-(sorti1(94 ^ []))],extension(96 ^ 8)).
% 0.88/1.40 ncf('1.1.2.1.1.2',plain,[-(sorti2(h(91 ^ []))), sorti1(91 ^ [])],extension(110 ^ 5,bind([[_31580], [91 ^ []]]))).
% 0.88/1.40 ncf('1.1.2.1.1.2.1',plain,[-(sorti1(91 ^ []))],extension(93 ^ 6)).
% 0.88/1.40 ncf('1.1.2.2',plain,[-(j(op2(h(94 ^ []), h(91 ^ []))) = op1(94 ^ [], 91 ^ [])), j(op2(h(94 ^ []), h(91 ^ []))) = op1(j(h(94 ^ [])), j(h(91 ^ []))), op1(j(h(94 ^ [])), j(h(91 ^ []))) = op1(94 ^ [], 91 ^ [])],extension(10 ^ 3,bind([[_28242, _28244, _28246], [op1(94 ^ [], 91 ^ []), op1(j(h(94 ^ [])), j(h(91 ^ []))), j(op2(h(94 ^ []), h(91 ^ [])))]]))).
% 0.88/1.40 ncf('1.1.2.2.1',plain,[-(j(op2(h(94 ^ []), h(91 ^ []))) = op1(j(h(94 ^ [])), j(h(91 ^ [])))), 136 : sorti2(h(91 ^ [])), 136 : sorti2(h(94 ^ []))],extension(132 ^ 4,bind([[_32309, _32451], [h(94 ^ []), h(91 ^ [])]]))).
% 0.88/1.40 ncf('1.1.2.2.1.1',plain,[-(sorti2(h(91 ^ []))), sorti1(91 ^ [])],extension(110 ^ 7,bind([[_31580], [91 ^ []]]))).
% 0.88/1.40 ncf('1.1.2.2.1.1.1',plain,[-(sorti1(91 ^ []))],extension(93 ^ 8)).
% 0.88/1.40 ncf('1.1.2.2.1.2',plain,[-(sorti2(h(94 ^ []))), sorti1(94 ^ [])],extension(110 ^ 5,bind([[_31580], [94 ^ []]]))).
% 0.88/1.40 ncf('1.1.2.2.1.2.1',plain,[-(sorti1(94 ^ []))],extension(96 ^ 6)).
% 0.88/1.40 ncf('1.1.2.2.2',plain,[-(op1(j(h(94 ^ [])), j(h(91 ^ []))) = op1(94 ^ [], 91 ^ [])), j(h(94 ^ [])) = 94 ^ [], j(h(91 ^ [])) = 91 ^ []],extension(50 ^ 4,bind([[_29520, _29522, _29524, _29526], [91 ^ [], j(h(91 ^ [])), 94 ^ [], j(h(94 ^ []))]]))).
% 0.88/1.40 ncf('1.1.2.2.2.1',plain,[-(j(h(94 ^ [])) = 94 ^ []), sorti1(94 ^ [])],extension(148 ^ 5,bind([[_32852], [94 ^ []]]))).
% 0.88/1.40 ncf('1.1.2.2.2.1.1',plain,[-(sorti1(94 ^ []))],extension(96 ^ 6)).
% 0.88/1.40 ncf('1.1.2.2.2.2',plain,[-(j(h(91 ^ [])) = 91 ^ []), sorti1(91 ^ [])],extension(148 ^ 5,bind([[_32852], [91 ^ []]]))).
% 0.88/1.40 ncf('1.1.2.2.2.2.1',plain,[-(sorti1(91 ^ []))],extension(93 ^ 6)).
% 0.88/1.40 %-----------------------------------------------------
% 0.88/1.40 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------